path: "vendor/opentheory/data/theories/relation-well-founded-def/relation-well-founded-def.art"
6 version nil "P" "->" typeOp 0 def 0 ref "A" varType 1 def 0 ref 1 ref "bool" typeOp nil opType 2 def nil cons 3 def cons opType 4 def nil cons cons opType 5 def 3 ref cons opType 6 def var "r" 5 ref var 7 def "=" const 8 def 0 ref 2 ref 0 ref 2 ref 3 ref cons opType 9 def nil cons cons opType 10 def constTerm 11 def "Relation.wellFounded" "_11270" 5 ref var 12 def "Data.Bool.!" const 13 def 0 ref 0 ref 4 ref 3 ref cons opType 14 def 3 ref cons opType 15 def constTerm 16 def "p" 4 ref var 17 def "Data.Bool.==>" const 10 ref constTerm 18 def "Data.Bool.?" const 14 ref constTerm 19 def "x" 1 ref var 20 def 17 ref varTerm 21 def 20 ref varTerm 22 def appTerm 23 def absTerm appTerm appTerm 24 def 19 ref 20 ref "Data.Bool./\\" const 10 remove constTerm 23 remove appTerm 25 def 13 ref 14 ref constTerm 26 def "y" 1 remove var 27 def 18 ref 12 ref varTerm 28 def 27 ref varTerm 29 def appTerm 22 ref appTerm appTerm "Data.Bool.~" const 9 remove constTerm 21 ref 29 ref appTerm appTerm 30 def appTerm absTerm appTerm appTerm absTerm appTerm appTerm absTerm appTerm 31 def absTerm 32 def defineConst 33 def pop 6 ref constTerm 34 def 7 remove varTerm 35 def appTerm appTerm 16 remove 17 ref 24 remove 19 remove 20 ref 25 remove 26 ref 27 remove 18 remove 35 remove 29 remove appTerm 22 remove appTerm appTerm 30 remove appTerm absTerm appTerm appTerm absTerm appTerm appTerm absTerm appTerm appTerm absTerm 36 def nil cons cons nil cons nil cons cons "A" 5 remove nil cons cons nil cons nil nil cons cons 11 ref 26 ref "P" 4 ref var varTerm 37 def appTerm appTerm refl 17 remove 8 ref 0 ref 4 remove 14 ref nil cons cons opType constTerm 21 remove appTerm 20 remove "Data.Bool.T" const 2 ref constTerm 38 def absTerm appTerm absTerm 39 def 37 ref appTerm betaConv appThm nil 8 remove 0 ref 14 remove 15 remove nil cons cons opType constTerm 26 remove appTerm 39 remove appTerm axiom 37 remove refl appThm eqMp sym subst subst 12 remove nil "t" 2 remove var 40 def 11 ref 34 remove 28 ref appTerm appTerm 31 remove appTerm nil cons cons nil cons nil cons cons 11 remove 40 remove varTerm 41 def appTerm 38 ref appTerm assume sym nil 38 remove axiom 42 def eqMp 41 remove assume 42 remove deductAntisym deductAntisym subst 33 remove 28 ref refl appThm 32 remove 28 remove appTerm betaConv trans eqMp absThm eqMp nil 13 remove 0 remove 6 remove 3 remove cons opType constTerm 36 remove appTerm thm