path: "vendor/opentheory/data/theories/set-size-def/set-size-def.art"
6 version "Set.size" "Set.fold" const "->" typeOp 0 def 0 ref "A" varType 1 def 0 ref "Number.Natural.natural" typeOp nil opType 2 def 2 ref nil cons 3 def cons opType 4 def nil cons cons opType 0 ref 2 ref 0 ref "Set.set" typeOp 1 ref nil cons opType 5 def 3 ref cons opType 6 def nil cons cons opType nil cons cons opType constTerm "x" 1 ref var 7 def "n" 2 ref var 8 def "Number.Natural.suc" const 4 remove constTerm 8 ref varTerm 9 def appTerm absTerm absTerm appTerm "Number.Natural.zero" const 2 ref constTerm appTerm 10 def defineConst 11 def pop 12 def pop 11 remove nil "=" const 13 def 0 ref 6 ref 0 ref 6 ref "bool" typeOp nil opType 14 def nil cons 15 def cons opType nil cons cons opType constTerm 12 remove 6 remove constTerm 16 def appTerm 10 remove appTerm thm nil "P" 0 ref 5 ref 15 ref cons opType 17 def var "s" 5 ref var 18 def "Data.Bool.!" const 19 def 0 ref 0 ref 2 ref 15 ref cons opType 20 def 15 ref cons opType constTerm 21 def 8 remove 13 ref 0 ref 14 ref 0 ref 14 ref 15 ref cons opType nil cons cons opType 22 def constTerm 23 def "Set.hasSize" "_10120" 5 ref var 24 def "_10121" 2 ref var 25 def "Data.Bool./\\" const 22 remove constTerm 26 def "Set.finite" const 17 ref constTerm 27 def 24 ref varTerm 28 def appTerm appTerm 13 ref 0 ref 2 remove 20 ref nil cons 29 def cons opType constTerm 30 def 16 ref 28 ref appTerm appTerm 25 ref varTerm 31 def appTerm appTerm 32 def absTerm 33 def absTerm 34 def defineConst 35 def pop 0 ref 5 ref 29 remove cons opType constTerm 36 def 18 remove varTerm 37 def appTerm 9 ref appTerm appTerm 26 remove 27 remove 37 ref appTerm appTerm 30 remove 16 remove 37 remove appTerm appTerm 9 remove appTerm appTerm appTerm absTerm appTerm absTerm 38 def nil cons cons nil cons nil cons cons "A" 5 remove nil cons cons nil cons nil nil cons 39 def cons 23 ref 19 ref 0 ref 0 ref 1 remove 15 ref cons opType 40 def 15 ref cons opType 41 def constTerm 42 def "P" 40 ref var varTerm 43 def appTerm appTerm refl "p" 40 ref var 44 def 13 ref 0 ref 40 remove 41 ref nil cons cons opType constTerm 44 remove varTerm appTerm 7 remove "Data.Bool.T" const 14 ref constTerm 45 def absTerm appTerm absTerm 46 def 43 ref appTerm betaConv appThm nil 13 remove 0 ref 41 ref 0 ref 41 remove 15 ref cons opType nil cons cons opType constTerm 42 remove appTerm 46 remove appTerm axiom 43 remove refl appThm eqMp sym 47 def subst subst 24 remove nil "t" 14 remove var 48 def 21 remove 25 ref 23 ref 36 remove 28 ref appTerm 31 ref appTerm appTerm 32 remove appTerm 49 def absTerm 50 def appTerm nil cons cons nil cons nil cons cons 23 remove 48 ref varTerm 51 def appTerm 45 ref appTerm assume sym nil 45 remove axiom 52 def eqMp 51 remove assume 52 remove deductAntisym deductAntisym 53 def subst nil "P" 20 remove var 50 remove nil cons cons nil cons nil cons cons "A" 3 remove cons nil cons 39 remove cons 47 remove subst subst 25 remove nil 48 remove 49 remove nil cons cons nil cons nil cons cons 53 remove subst 35 remove 28 ref refl appThm 34 remove 28 remove appTerm betaConv trans 31 ref refl appThm 33 remove 31 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 19 remove 0 remove 17 remove 15 remove cons opType constTerm 38 remove appTerm thm