ZF Set Theory (in FOL) val it = () : unit - stamps: ProtoPure Pure IFOL FOL Let ZF classes: term logic subclass: logic < term < logic default: term types: is 0 pttrns 0 i 0 letbinds 0 letbind 0 o 0 fun 2 prop 0 itself 1 id 0 var 0 tid 0 tvar 0 xnum 0 xstr 0 logic 0 type 0 types 0 sort 0 classes 0 args 0 cargs 0 pttrn 0 idt 0 idts 0 aprop 0 asms 0 any 0 #prop 0 abbrs: arities: i :: logic i :: term o :: logic fun :: (logic, logic) logic prop :: logic itself :: (logic) logic consts: "0" :: "i" "==" :: "[?'a, ?'a] => prop" "==>" :: "[prop, prop] => prop" "=?=" :: "[?'a, ?'a] => prop" "All" :: "(?'a => o) => o" "Ball" :: "[i, i => o] => o" "Bex" :: "[i, i => o] => o" "Collect" :: "[i, i => o] => i" "Ex" :: "(?'a => o) => o" "Ex1" :: "(?'a => o) => o" "False" :: "o" "Inf" :: "i" "Inter" :: "i => i" "Lambda" :: "[i, i => i] => i" "Let" :: "[?'a, ?'a => ?'b] => ?'b" "Not" :: "o => o" "Pair" :: "[i, i] => i" "Pi" :: "[i, i => i] => i" "Pow" :: "i => i" "PrimReplace" :: "[i, [i, i] => o] => i" "RepFun" :: "[i, i => i] => i" "Replace" :: "[i, [i, i] => o] => i" "Sigma" :: "[i, i => i] => i" "TYPE" :: "?'a itself" "The" :: "(i => o) => i" "True" :: "o" "Trueprop" :: "o => prop" "Union" :: "i => i" "Upair" :: "[i, i] => i" "all" :: "(?'a => prop) => prop" "cons" :: "[i, i] => i" "converse" :: "i => i" "domain" :: "i => i" "field" :: "i => i" "fst" :: "i => i" "function" :: "i => o" "if" :: "[o, i, i] => i" "logic_class" :: "?'a itself => prop" "op &" :: "[o, o] => o" "op -" :: "[i, i] => i" "op -->" :: "[o, o] => o" "op -``" :: "[i, i] => i" "op :" :: "[i, i] => o" "op <->" :: "[o, o] => o" "op <=" :: "[i, i] => o" "op =" :: "[?'a, ?'a] => o" "op Int" :: "[i, i] => i" "op Un" :: "[i, i] => i" "op `" :: "[i, i] => i" "op ``" :: "[i, i] => i" "op |" :: "[o, o] => o" "range" :: "i => i" "restrict" :: "[i, i] => i" "snd" :: "i => i" "split" :: "[[i, i] => ?'a, i] => ?'a" "succ" :: "i => i" "term_class" :: "?'a itself => prop" additional axioms: Ball_def: "Ball(?A, ?P) == ALL x. x : ?A --> ?P(x)" Bex_def: "Bex(?A, ?P) == EX x. x : ?A & ?P(x)" Collect_def: "Collect(?A, ?P) == {y . x: ?A, x = y & ?P(x)}" Diff_def: "?A - ?B == {x: ?A . x ~: ?B}" Int_def: "?A Int ?B == Inter(Upair(?A, ?B))" Inter_def: "Inter(?A) == {x: Union(?A) . ALL y:?A. x : y}" Pair_def: " == {{?a, ?a}, {?a, ?b}}" Pi_def: "Pi(?A, ?B) == {f: Pow(Sigma(?A, ?B)) . ?A <= domain(f) & function(f)}" Pow_iff: "?A : Pow(?B) <-> ?A <= ?B" RepFun_def: "RepFun(?A, ?f) == {y . x: ?A, y = ?f(x)}" Replace_def: "Replace(?A, ?P) == PrimReplace(?A, %x y. (EX! z. ?P(x, z)) & ?P(x, y))" Sigma_def: "Sigma(?A, ?B) == UN x:?A. UN y:?B(x). {}" Un_def: "?A Un ?B == Union(Upair(?A, ?B))" Union_iff: "?A : Union(?C) <-> (EX B:?C. ?A : B)" Upair_def: "Upair(?a, ?b) == {y . x: Pow(Pow(0)), x = 0 & y = ?a | x = Pow(0) & y = ?b}" apply_def: "?f ` ?a == THE y. : ?f" cons_def: "cons(?a, ?A) == Upair(?a, ?a) Un ?A" converse_def: "converse(?r) == {z . w: ?r, EX x y. w = & z = }" domain_def: "domain(?r) == {x . w: ?r, EX y. w = }" extension: "?A = ?B <-> ?A <= ?B & ?B <= ?A" field_def: "field(?r) == domain(?r) Un range(?r)" foundation: "?A = 0 | (EX x:?A. ALL y:x. y ~: ?A)" fst_def: "fst(?p) == THE a. EX b. ?p = " function_def: "function(?r) == ALL x y. : ?r --> (ALL y'. : ?r --> y = y')" if_def: "if(?P, ?a, ?b) == THE z. ?P & z = ?a | ~ ?P & z = ?b" image_def: "?r `` ?A == {y: range(?r) . EX x:?A. : ?r}" infinity: "0 : Inf & (ALL y:Inf. succ(y) : Inf)" lam_def: "Lambda(?A, ?b) == { . x: ?A}" range_def: "range(?r) == domain(converse(?r))" replacement: "ALL x:?A. ALL y z. ?P(x, y) & ?P(x, z) --> y = z ==> ?b : PrimReplace(?A, ?P) <-> (EX x:?A. ?P(x, ?b))" restrict_def: "restrict(?f, ?A) == lam x:?A. ?f ` x" snd_def: "snd(?p) == THE b. EX a. ?p = " split_def: "split(?c, ?p) == ?c(fst(?p), snd(?p))" subset_def: "?A <= ?B == ALL x:?A. x : ?B" succ_def: "succ(?i) == cons(?i, ?i)" the_def: "The(?P) == Union({y . x: {0}, ?P(y)})" vimage_def: "?r -`` ?A == converse(?r) `` ?A" stored theorems: CollectD1: "?a : {x: ?A . ?P(x)} ==> ?a : ?A" CollectD2: "?a : {x: ?A . ?P(x)} ==> ?P(?a)" CollectE: "[| ?a : {x: ?A . ?P(x)}; [| ?a : ?A; ?P(?a) |] ==> ?R |] ==> ?R" CollectI: "[| ?a : ?A; ?P(?a) |] ==> ?a : {x: ?A . ?P(x)}" Collect_cong: "[| ?A = ?B; !!x. x : ?B ==> ?P(x) <-> ?Q(x) |] ==> Collect(?A, ?P) = Collect(?B, ?Q)" Collect_mono: "[| ?A <= ?B; !!x. x : ?A ==> ?P(x) --> ?Q(x) |] ==> Collect(?A, ?P) <= Collect(?B, ?Q)" Collect_subset: "Collect(?A, ?P) <= ?A" DiffD1: "?c : ?A - ?B ==> ?c : ?A" DiffD2: "?c : ?A - ?B ==> ?c ~: ?B" DiffE: "[| ?c : ?A - ?B; [| ?c : ?A; ?c ~: ?B |] ==> ?P |] ==> ?P" DiffI: "[| ?c : ?A; ?c ~: ?B |] ==> ?c : ?A - ?B" Diff_0: "?A - 0 = ?A" Diff_INT: "?i : ?I ==> ?B - (INT i:?I. ?A(i)) = (UN i:?I. ?B - ?A(i))" Diff_Int: "?A - ?B Int ?C = ?A - ?B Un (?A - ?C)" Diff_UN: "?i : ?I ==> ?B - (UN i:?I. ?A(i)) = (INT i:?I. ?B - ?A(i))" Diff_Un: "?A - (?B Un ?C) = (?A - ?B) Int (?A - ?C)" Diff_cancel: "?A - ?A = 0" Diff_cons: "?A - cons(?a, ?B) = ?A - ?B - {?a}" Diff_cons2: "?A - cons(?a, ?B) = ?A - {?a} - ?B" Diff_contains: "[| ?C <= ?A; ?C Int ?B = 0 |] ==> ?C <= ?A - ?B" Diff_disjoint: "?A Int (?B - ?A) = 0" Diff_eq_0_iff: "?A - ?B = 0 <-> ?A <= ?B" Diff_iff: "?c : ?A - ?B <-> ?c : ?A & ?c ~: ?B" Diff_mono: "[| ?A <= ?C; ?D <= ?B |] ==> ?A - ?B <= ?C - ?D" Diff_partition: "?A <= ?B ==> ?A Un (?B - ?A) = ?B" Diff_subset: "?A - ?B <= ?A" INT_E: "[| ?b : (INT x:?A. ?B(x)); ?a : ?A |] ==> ?b : ?B(?a)" INT_I: "[| !!x. x : ?A ==> ?b : ?B(x); ?a : ?A |] ==> ?b : (INT x:?A. ?B(x))" INT_Int_distrib: "?i : ?I ==> (INT i:?I. ?A(i) Int ?B(i)) = (INT i:?I. ?A(i)) Int (INT i:?I. ?B(i))" INT_Pow_subset: "?x : ?A ==> (INT x:?A. Pow(?B(x))) = Pow(INT x:?A. ?B(x))" INT_cong: "[| ?A = ?B; !!x. x : ?B ==> ?C(x) = ?D(x) |] ==> (INT x:?A. ?C(x)) = (INT x:?B. ?D(x))" INT_constant: "?a : ?A ==> (INT y:?A. ?c) = ?c" INT_greatest: "[| ?a : ?A; !!x. x : ?A ==> ?C <= ?B(x) |] ==> ?C <= (INT x:?A. ?B(x))" INT_iff: "?b : (INT x:?A. ?B(x)) <-> (ALL x:?A. ?b : ?B(x)) & (EX x. x : ?A)" INT_lower: "?x : ?A ==> (INT x:?A. ?B(x)) <= ?B(?x)" IntD1: "?c : ?A Int ?B ==> ?c : ?A" IntD2: "?c : ?A Int ?B ==> ?c : ?B" IntE: "[| ?c : ?A Int ?B; [| ?c : ?A; ?c : ?B |] ==> ?P |] ==> ?P" IntI: "[| ?c : ?A; ?c : ?B |] ==> ?c : ?A Int ?B" Int_0: "0 Int ?A = 0" Int_Diff_eq: "?C <= ?A ==> (?A - ?B) Int ?C = ?C - ?B" Int_Pow_eq: "Pow(?A) Int Pow(?B) = Pow(?A Int ?B)" Int_UN_distrib: "?B Int (UN i:?I. ?A(i)) = (UN i:?I. ?B Int ?A(i))" Int_UN_distrib2: "(UN i:?I. ?A(i)) Int (UN j:?J. ?B(j)) = (UN i:?I. UN j:?J. ?A(i) Int ?B(j))" Int_Un_distrib: "(?A Un ?B) Int ?C = ?A Int ?C Un ?B Int ?C" Int_absorb: "?A Int ?A = ?A" Int_assoc: "?A Int ?B Int ?C = ?A Int (?B Int ?C)" Int_commute: "?A Int ?B = ?B Int ?A" Int_cons: "cons(?a, ?B) Int ?C <= cons(?a, ?B Int ?C)" Int_greatest: "[| ?C <= ?A; ?C <= ?B |] ==> ?C <= ?A Int ?B" Int_iff: "?c : ?A Int ?B <-> ?c : ?A & ?c : ?B" Int_lower1: "?A Int ?B <= ?A" Int_lower2: "?A Int ?B <= ?B" Int_mono: "[| ?A <= ?C; ?B <= ?D |] ==> ?A Int ?B <= ?C Int ?D" Int_subset_iff: "?C <= ?A Int ?B <-> ?C <= ?A & ?C <= ?B" InterD: "[| ?A : Inter(?C); ?B : ?C |] ==> ?A : ?B" InterE: "[| ?A : Inter(?C); ?A : ?B ==> ?R; ?B ~: ?C ==> ?R |] ==> ?R" InterI: "[| !!x. x : ?C ==> ?A : x; ?c : ?C |] ==> ?A : Inter(?C)" Inter_Un_distrib: "[| ?a : ?A; ?b : ?B |] ==> Inter(?A Un ?B) = Inter(?A) Int Inter(?B)" Inter_anti_mono: "[| ?A <= ?B; ?a : ?A |] ==> Inter(?B) <= Inter(?A)" Inter_eq_INT: "Inter(?A) = (INT x:?A. x)" Inter_greatest: "[| ?a : ?A; !!x. x : ?A ==> ?C <= x |] ==> ?C <= Inter(?A)" Inter_iff: "?A : Inter(?C) <-> (ALL x:?C. ?A : x) & (EX x. x : ?C)" Inter_lemma0: "[| ?c : ?C; ALL x:?C. ?A <= x | x <= ?B |] ==> ?A <= Inter(?C) | Inter(?C) <= ?B" Inter_lower: "?B : ?A ==> Inter(?A) <= ?B" Inter_singleton: "Inter({?b}) = ?b" Inter_subset_iff: "?a : ?A ==> ?C <= Inter(?A) <-> (ALL x:?A. ?C <= x)" Pair_fst_snd_eq: "?a : Sigma(?A, ?B) ==> = ?a" Pair_iff: " = <-> ?a = ?c & ?b = ?d" Pair_inject: "[| = ; [| ?a = ?c; ?b = ?d |] ==> ?R |] ==> ?R" Pair_inject1: " = ==> ?a = ?c" Pair_inject2: " = ==> ?b = ?d" Pair_mem_PiE: "[| : ?f; ?f : Pi(?A, ?B); [| ?a : ?A; ?b : ?B(?a); ?f ` ?a = ?b |] ==> ?P |] ==> ?P" Pair_neq_0: " = 0 ==> ?P" Pair_neq_fst: " = ?a ==> ?P" Pair_neq_snd: " = ?b ==> ?P" Pi_cong: "[| ?A = ?A'; !!x. x : ?A' ==> ?B(x) = ?B'(x) |] ==> Pi(?A, ?B) = Pi(?A', ?B')" Pi_empty1: "Pi(0, ?A) = {0}" Pi_empty2: "?a : ?A ==> ?A -> 0 = 0" Pi_iff: "?f : Pi(?A, ?B) <-> function(?f) & ?f <= Sigma(?A, ?B) & ?A <= domain(?f)" Pi_iff_old: "?f : Pi(?A, ?B) <-> ?f <= Sigma(?A, ?B) & (ALL x:?A. EX! y. : ?f)" Pi_lamE: "[| ?f : Pi(?A, ?B); !!b. [| ALL x:?A. b(x) : ?B(x); ?f = (lam x:?A. b(x)) |] ==> ?P |] ==> ?P" Pi_memberD: "[| ?f : Pi(?A, ?B); ?c : ?f |] ==> EX x:?A. ?c = " Pi_mono: "?B <= ?C ==> ?A -> ?B <= ?A -> ?C" Pi_type: "[| ?f : Pi(?A, ?C); !!x. x : ?A ==> ?f ` x : ?B(x) |] ==> ?f : Pi(?A, ?B)" PowD: "?A : Pow(?B) ==> ?A <= ?B" PowI: "?A <= ?B ==> ?A : Pow(?B)" Pow_mono: "?A <= ?B ==> Pow(?A) <= Pow(?B)" RepFunE: "[| ?b : {?f(x) . x: ?A}; !!x. [| x : ?A; ?b = ?f(x) |] ==> ?P |] ==> ?P" RepFunI: "?a : ?A ==> ?f(?a) : {?f(x) . x: ?A}" RepFun_0: "{?f(x) . x: 0} = 0" RepFun_cong: "[| ?A = ?B; !!x. x : ?B ==> ?f(x) = ?g(x) |] ==> RepFun(?A, ?f) = RepFun(?B, ?g)" RepFun_eqI: "[| ?b = ?f(?a); ?a : ?A |] ==> ?b : {?f(x) . x: ?A}" RepFun_eq_0_iff: "{?f(x) . x: ?A} = 0 <-> ?A = 0" RepFun_iff: "?b : {?f(x) . x: ?A} <-> (EX x:?A. ?b = ?f(x))" RepFun_mono: "?A <= ?B ==> {?f(x) . x: ?A} <= {?f(x) . x: ?B}" RepFun_subset: "(!!x. x : ?A ==> ?f(x) : ?B) ==> {?f(x) . x: ?A} <= ?B" ReplaceE: "[| ?b : {y . x: ?A, ?P(x, y)}; !!x. [| x : ?A; ?P(x, ?b); ALL y. ?P(x, y) --> y = ?b |] ==> ?R |] ==> ?R" ReplaceE2: "[| ?b : {y . x: ?A, ?P(x, y)}; !!x. [| x : ?A; ?P(x, ?b) |] ==> ?R |] ==> ?R" ReplaceI: "[| ?P(?x, ?b); ?x : ?A; !!y. ?P(?x, y) ==> y = ?b |] ==> ?b : {y . x: ?A, ?P(x, y)}" Replace_cong: "[| ?A = ?B; !!x y. x : ?B ==> ?P(x, y) <-> ?Q(x, y) |] ==> Replace(?A, ?P) = Replace(?B, ?Q)" Replace_iff: "?b : {y . x: ?A, ?P(x, y)} <-> (EX x:?A. ?P(x, ?b) & (ALL y. ?P(x, y) --> y = ?b))" Replace_mono: "?A <= ?B ==> Replace(?A, ?P) <= Replace(?B, ?P)" SUM_Int_distrib1: "(SUM i:?I Int ?J. ?C(i)) = (SUM i:?I. ?C(i)) Int (SUM j:?J. ?C(j))" SUM_Int_distrib2: "(SUM i:?I. ?A(i) Int ?B(i)) = (SUM i:?I. ?A(i)) Int (SUM i:?I. ?B(i))" SUM_UN_distrib1: "(SUM x:UN y:?A. ?C(y). ?B(x)) = (UN y:?A. SUM x:?C(y). ?B(x))" SUM_UN_distrib2: "(SUM i:?I. UN j:?J. ?C(i, j)) = (UN j:?J. SUM i:?I. ?C(i, j))" SUM_Un_distrib1: "(SUM i:?I Un ?J. ?C(i)) = (SUM i:?I. ?C(i)) Un (SUM j:?J. ?C(j))" SUM_Un_distrib2: "(SUM i:?I. ?A(i) Un ?B(i)) = (SUM i:?I. ?A(i)) Un (SUM i:?I. ?B(i))" SUM_eq_UN: "(SUM i:?I. ?A(i)) = (UN i:?I. {i} * ?A(i))" SigmaD1: " : Sigma(?A, ?B) ==> ?a : ?A" SigmaD2: " : Sigma(?A, ?B) ==> ?b : ?B(?a)" SigmaE: "[| ?c : Sigma(?A, ?B); !!x y. [| x : ?A; y : ?B(x); ?c = |] ==> ?P |] ==> ?P" SigmaE2: "[| : Sigma(?A, ?B); [| ?a : ?A; ?b : ?B(?a) |] ==> ?P |] ==> ?P" SigmaI: "[| ?a : ?A; ?b : ?B(?a) |] ==> : Sigma(?A, ?B)" Sigma_cong: "[| ?A = ?A'; !!x. x : ?A' ==> ?B(x) = ?B'(x) |] ==> Sigma(?A, ?B) = Sigma(?A', ?B')" Sigma_cons: "Sigma(cons(?a, ?B), ?C) = {?a} * ?C(?a) Un Sigma(?B, ?C)" Sigma_empty1: "Sigma(0, ?B) = 0" Sigma_empty2: "?A * 0 = 0" Sigma_mono_lemma: "[| ?A <= ?C; ALL x:?A. ?B(x) <= ?D(x) |] ==> Sigma(?A, ?B) <= Sigma(?C, ?D)" UN_0: "(UN i:0. ?A(i)) = 0" UN_E: "[| ?b : (UN x:?A. ?B(x)); !!x. [| x : ?A; ?b : ?B(x) |] ==> ?R |] ==> ?R" UN_I: "[| ?a : ?A; ?b : ?B(?a) |] ==> ?b : (UN x:?A. ?B(x))" UN_Pow_subset: "(UN x:?A. Pow(?B(x))) <= Pow(UN x:?A. ?B(x))" UN_Un_distrib: "(UN i:?I. ?A(i) Un ?B(i)) = (UN i:?I. ?A(i)) Un (UN i:?I. ?B(i))" UN_cong: "[| ?A = ?B; !!x. x : ?B ==> ?C(x) = ?D(x) |] ==> (UN x:?A. ?C(x)) = (UN x:?B. ?D(x))" UN_constant: "?a : ?A ==> (UN y:?A. ?c) = ?c" UN_iff: "?b : (UN x:?A. ?B(x)) <-> (EX x:?A. ?b : ?B(x))" UN_least: "(!!x. x : ?A ==> ?B(x) <= ?C) ==> (UN x:?A. ?B(x)) <= ?C" UN_mono: "[| ?A <= ?C; !!x. x : ?A ==> ?B(x) <= ?D(x) |] ==> (UN x:?A. ?B(x)) <= (UN x:?C. ?D(x))" UN_subset_iff: "(UN x:?A. ?B(x)) <= ?C <-> (ALL x:?A. ?B(x) <= ?C)" UN_upper: "?x : ?A ==> ?B(?x) <= (UN x:?A. ?B(x))" UnCI: "(?c ~: ?B ==> ?c : ?A) ==> ?c : ?A Un ?B" UnE: "[| ?c : ?A Un ?B; ?c : ?A ==> ?P; ?c : ?B ==> ?P |] ==> ?P" UnE': "[| ?c : ?A Un ?B; ?c : ?A ==> ?P; [| ?c : ?B; ?c ~: ?A |] ==> ?P |] ==> ?P" UnI1: "?c : ?A ==> ?c : ?A Un ?B" UnI2: "?c : ?B ==> ?c : ?A Un ?B" Un_0: "0 Un ?A = ?A" Un_INT_distrib: "?i : ?I ==> ?B Un (INT i:?I. ?A(i)) = (INT i:?I. ?B Un ?A(i))" Un_INT_distrib2: "[| ?i : ?I; ?j : ?J |] ==> (INT i:?I. ?A(i)) Un (INT j:?J. ?B(j)) = (INT i:?I. INT j:?J. ?A(i) Un ?B(j))" Un_Int_assoc_iff: "?A Int ?B Un ?C = ?A Int (?B Un ?C) <-> ?C <= ?A" Un_Int_crazy: "?A Int ?B Un ?B Int ?C Un ?C Int ?A = (?A Un ?B) Int (?B Un ?C) Int (?C Un ?A)" Un_Int_distrib: "?A Int ?B Un ?C = (?A Un ?C) Int (?B Un ?C)" Un_Pow_subset: "Pow(?A) Un Pow(?B) <= Pow(?A Un ?B)" Un_absorb: "?A Un ?A = ?A" Un_assoc: "?A Un ?B Un ?C = ?A Un (?B Un ?C)" Un_commute: "?A Un ?B = ?B Un ?A" Un_cons: "cons(?a, ?B) Un ?C = cons(?a, ?B Un ?C)" Un_iff: "?c : ?A Un ?B <-> ?c : ?A | ?c : ?B" Un_least: "[| ?A <= ?C; ?B <= ?C |] ==> ?A Un ?B <= ?C" Un_mono: "[| ?A <= ?C; ?B <= ?D |] ==> ?A Un ?B <= ?C Un ?D" Un_subset_iff: "?A Un ?B <= ?C <-> ?A <= ?C & ?B <= ?C" Un_upper1: "?A <= ?A Un ?B" Un_upper2: "?B <= ?A Un ?B" UnionE: "[| ?A : Union(?C); !!B. [| ?A : B; B : ?C |] ==> ?R |] ==> ?R" UnionI: "[| ?B : ?C; ?A : ?B |] ==> ?A : Union(?C)" Union_0: "Union(0) = 0" Union_Int_subset: "Union(?A Int ?B) <= Union(?A) Int Union(?B)" Union_Pow_eq: "Union(Pow(?A)) = ?A" Union_Un_distrib: "Union(?A Un ?B) = Union(?A) Un Union(?B)" Union_cons: "Union(cons(?a, ?B)) = ?a Un Union(?B)" Union_disjoint: "Union(?C) Int ?A = 0 <-> (ALL B:?C. B Int ?A = 0)" Union_eq_UN: "Union(?A) = (UN x:?A. x)" Union_in_Pow: "?Y : Pow(Pow(?A)) ==> Union(?Y) : Pow(?A)" Union_least: "(!!x. x : ?A ==> x <= ?C) ==> Union(?A) <= ?C" Union_lemma0: "ALL x:?C. x <= ?A | ?B <= x ==> Union(?C) <= ?A | ?B <= Union(?C)" Union_mono: "?A <= ?B ==> Union(?A) <= Union(?B)" Union_singleton: "Union({?b}) = ?b" Union_subset_iff: "Union(?A) <= ?C <-> (ALL x:?A. x <= ?C)" Union_upper: "?B : ?A ==> ?B <= Union(?A)" UpairE: "[| ?a : Upair(?b, ?c); ?a = ?b ==> ?P; ?a = ?c ==> ?P |] ==> ?P" UpairI1: "?a : Upair(?a, ?b)" UpairI2: "?b : Upair(?a, ?b)" apply_0: "[| ?a ~: domain(?f); ?f : Pi(?A, ?B) |] ==> ?f ` ?a = 0" apply_Pair: "[| ?f : Pi(?A, ?B); ?a : ?A |] ==> : ?f" apply_equality: "[| : ?f; ?f : Pi(?A, ?B) |] ==> ?f ` ?a = ?b" apply_equality2: "[| : ?f; : ?f; ?f : Pi(?A, ?B) |] ==> ?b = ?c" apply_funtype: "[| ?f : ?A -> ?B; ?a : ?A |] ==> ?f ` ?a : ?B" apply_iff: "?f : Pi(?A, ?B) ==> : ?f <-> ?a : ?A & ?f ` ?a = ?b" apply_rangeI: "[| ?f : Pi(?A, ?B); ?a : ?A |] ==> ?f ` ?a : range(?f)" apply_type: "[| ?f : Pi(?A, ?B); ?a : ?A |] ==> ?f ` ?a : ?B(?a)" ballE: "[| ALL x:?A. ?P(x); ?P(?x) ==> ?Q; ?x ~: ?A ==> ?Q |] ==> ?Q" ballI: "(!!x. x : ?A ==> ?P(x)) ==> ALL x:?A. ?P(x)" ball_cong: "[| ?A = ?A'; !!x. x : ?A' ==> ?P(x) <-> ?P'(x) |] ==> Ball(?A, ?P) <-> Ball(?A', ?P')" ball_simp: "(ALL x:?A. True) <-> True" beta: "?a : ?A ==> (lam x:?A. ?b(x)) ` ?a = ?b(?a)" bexCI: "[| ALL x:?A. ~ ?P(x) ==> ?P(?a); ?a : ?A |] ==> EX x:?A. ?P(x)" bexE: "[| EX x:?A. ?P(x); !!x. [| x : ?A; ?P(x) |] ==> ?Q |] ==> ?Q" bexI: "[| ?P(?x); ?x : ?A |] ==> EX x:?A. ?P(x)" bex_cong: "[| ?A = ?A'; !!x. x : ?A' ==> ?P(x) <-> ?P'(x) |] ==> Bex(?A, ?P) <-> Bex(?A', ?P')" bspec: "[| ALL x:?A. ?P(x); ?x : ?A |] ==> ?P(?x)" cantor: "EX S:Pow(?A). ALL x:?A. ?b(x) ~= S" consCI: "(?a ~: ?B ==> ?a = ?b) ==> ?a : cons(?b, ?B)" consE: "[| ?a : cons(?b, ?A); ?a = ?b ==> ?P; ?a : ?A ==> ?P |] ==> ?P" consE': "[| ?a : cons(?b, ?A); ?a = ?b ==> ?P; [| ?a : ?A; ?a ~= ?b |] ==> ?P |] ==> ?P" consI1: "?a : cons(?a, ?B)" consI2: "?a : ?B ==> ?a : cons(?b, ?B)" cons_Diff: "?a : ?B ==> cons(?a, ?B - {?a}) = ?B" cons_absorb: "?a : ?B ==> cons(?a, ?B) = ?B" cons_commute: "cons(?a, cons(?b, ?C)) = cons(?b, cons(?a, ?C))" cons_eq: "{?a} Un ?B = cons(?a, ?B)" cons_fun_eq: "?c ~: ?A ==> cons(?c, ?A) -> ?B = (UN f:?A -> ?B. UN b:?B. {cons(, f)})" cons_iff: "?a : cons(?b, ?A) <-> ?a = ?b | ?a : ?A" cons_mono: "?C <= ?D ==> cons(?a, ?C) <= cons(?a, ?D)" cons_subsetE: "[| cons(?a, ?B) <= ?C; [| ?a : ?C; ?B <= ?C |] ==> ?R |] ==> ?R" cons_subsetI: "[| ?a : ?C; ?B <= ?C |] ==> cons(?a, ?B) <= ?C" cons_subset_iff: "cons(?a, ?B) <= ?C <-> ?a : ?C & ?B <= ?C" converseD: " : converse(?r) ==> : ?r" converseE: "[| ?yx : converse(?r); !!x y. [| ?yx = ; : ?r |] ==> ?P |] ==> ?P" converseI: " : ?r ==> : converse(?r)" converse_Diff: "converse(?A) - converse(?B) = converse(?A - ?B)" converse_Int: "converse(?A Int ?B) = converse(?A) Int converse(?B)" converse_UN: "converse(UN x:?A. ?B(x)) = (UN x:?A. converse(?B(x)))" converse_Un: "converse(?A Un ?B) = converse(?A) Un converse(?B)" converse_converse: "?r <= Sigma(?A, ?B) ==> converse(converse(?r)) = ?r" converse_empty: "converse(0) = 0" converse_iff: " : converse(?r) <-> : ?r" converse_mono: "?r <= ?s ==> converse(?r) <= converse(?s)" converse_prod: "converse(?A * ?B) = ?B * ?A" converse_type: "?r <= ?A * ?B ==> converse(?r) <= ?B * ?A" domainE: "[| ?a : domain(?r); !!y. : ?r ==> ?P |] ==> ?P" domainI: " : ?r ==> ?a : domain(?r)" domain_0: "domain(0) = 0" domain_Diff_subset: "domain(?A) - domain(?B) <= domain(?A - ?B)" domain_Int_subset: "domain(?A Int ?B) <= domain(?A) Int domain(?B)" domain_Un_eq: "domain(?A Un ?B) = domain(?A) Un domain(?B)" domain_cons: "domain(cons(, ?r)) = cons(?a, domain(?r))" domain_converse: "domain(converse(?r)) = range(?r)" domain_iff: "?a : domain(?r) <-> (EX y. : ?r)" domain_mono: "?r <= ?s ==> domain(?r) <= domain(?s)" domain_of_fun: "?f : Pi(?A, ?B) ==> domain(?f) = ?A" domain_of_prod: "?b : ?B ==> domain(?A * ?B) = ?A" domain_rel_subset: "?r <= Sigma(?C, ?B) ==> domain(?r) <= ?C" domain_restrict: "domain(restrict(?f, ?C)) = ?C" domain_subset: "domain(Sigma(?A, ?B)) <= ?A" domain_subset_field: "domain(?r) <= field(?r)" domain_times_range: "?r <= Sigma(?A, ?B) ==> ?r <= domain(?r) * range(?r)" domain_type: "[| : ?f; ?f : Pi(?A, ?B) |] ==> ?a : ?A" double_complement: "[| ?A <= ?B; ?B <= ?C |] ==> ?B - (?C - ?A) = ?A" double_complement_Un: "?A Un ?B - (?B - ?A) = ?A" doubleton_eq_iff: "{?a, ?b} = {?c, ?d} <-> ?a = ?c & ?b = ?d | ?a = ?d & ?b = ?c" emptyE: "?a : 0 ==> ?P" empty_Diff: "0 - ?A = 0" empty_fun: "0 : Pi(0, ?B)" empty_subsetI: "0 <= ?A" equal_singleton_lemma: "[| ?a : ?C; ALL y:?C. y = ?b |] ==> ?C = {?b}" equalityCE: "[| ?A = ?B; [| ?c : ?A; ?c : ?B |] ==> ?P; [| ?c ~: ?A; ?c ~: ?B |] ==> ?P |] ==> ?P" equalityD1: "?A = ?B ==> ?A <= ?B" equalityD2: "?A = ?B ==> ?B <= ?A" equalityE: "[| ?A = ?B; [| ?A <= ?B; ?B <= ?A |] ==> ?P |] ==> ?P" equalityI: "[| ?A <= ?B; ?B <= ?A |] ==> ?A = ?B" equality_iffI: "(!!x. x : ?A <-> x : ?B) ==> ?A = ?B" equals0D: "[| ?A = 0; ?a : ?A |] ==> ?P" equals0I: "(!!y. y : ?A ==> False) ==> ?A = 0" eta: "?f : Pi(?A, ?B) ==> (lam x:?A. ?f ` x) = ?f" expand_if: "?P(if(?Q, ?x, ?y)) <-> (?Q --> ?P(?x)) & (~ ?Q --> ?P(?y))" expand_split: "?u : ?A * ?B ==> ?R(split(?c, ?u)) <-> (ALL x:?A. ALL y:?B. ?u = --> ?R(?c(x, y)))" fieldCI: "( ~: ?r ==> : ?r) ==> ?a : field(?r)" fieldE: "[| ?a : field(?r); !!x. : ?r ==> ?P; !!x. : ?r ==> ?P |] ==> ?P" fieldI1: " : ?r ==> ?a : field(?r)" fieldI2: " : ?r ==> ?b : field(?r)" field_0: "field(0) = 0" field_Diff_subset: "field(?A) - field(?B) <= field(?A - ?B)" field_Int_square: "field(?r Int ?A * ?A) <= ?A" field_Int_subset: "field(?A Int ?B) <= field(?A) Int field(?B)" field_Un_eq: "field(?A Un ?B) = field(?A) Un field(?B)" field_cons: "field(cons(, ?r)) = cons(?a, cons(?b, field(?r)))" field_mono: "?r <= ?s ==> field(?r) <= field(?s)" field_of_prod: "field(?A * ?A) = ?A" field_rel_subset: "?r <= ?A * ?A ==> field(?r) <= ?A" field_subset: "field(?A * ?B) <= ?A Un ?B" field_times_field: "?r <= Sigma(?A, ?B) ==> ?r <= field(?r) * field(?r)" fst_conv: "fst() = ?a" fst_type: "?p : Sigma(?A, ?B) ==> fst(?p) : ?A" fun_Union: "[| ALL f:?S. EX C D. f : C -> D; ALL f:?S. ALL y:?S. f <= y | y <= f |] ==> Union(?S) : domain(Union(?S)) -> range(Union(?S))" fun_disjoint_Un: "[| ?f : ?A -> ?B; ?g : ?C -> ?D; ?A Int ?C = 0 |] ==> ?f Un ?g : ?A Un ?C -> ?B Un ?D" fun_disjoint_apply1: "[| ?a : ?A; ?f : ?A -> ?B; ?g : ?C -> ?D; ?A Int ?C = 0 |] ==> (?f Un ?g) ` ?a = ?f ` ?a" fun_disjoint_apply2: "[| ?c : ?C; ?f : ?A -> ?B; ?g : ?C -> ?D; ?A Int ?C = 0 |] ==> (?f Un ?g) ` ?c = ?g ` ?c" fun_extend: "[| ?f : ?A -> ?B; ?c ~: ?A |] ==> cons(, ?f) : cons(?c, ?A) -> cons(?b, ?B)" fun_extend3: "[| ?f : ?A -> ?B; ?c ~: ?A; ?b : ?B |] ==> cons(, ?f) : cons(?c, ?A) -> ?B" fun_extend_apply1: "[| ?f : ?A -> ?B; ?a : ?A; ?c ~: ?A |] ==> cons(, ?f) ` ?a = ?f ` ?a" fun_extend_apply2: "[| ?f : ?A -> ?B; ?c ~: ?A |] ==> cons(, ?f) ` ?c = ?b" fun_extension: "[| ?f : Pi(?A, ?B); ?g : Pi(?A, ?D); !!x. x : ?A ==> ?f ` x = ?g ` x |] ==> ?f = ?g" fun_is_function: "?f : Pi(?A, ?B) ==> function(?f)" fun_is_rel: "?f : Pi(?A, ?B) ==> ?f <= Sigma(?A, ?B)" fun_subset: "[| ?f : Pi(?A, ?B); ?g : Pi(?C, ?D); ?A <= ?C; !!x. x : ?A ==> ?f ` x = ?g ` x |] ==> ?f <= ?g" fun_unique_Pair: "[| ?f : Pi(?A, ?B); ?a : ?A |] ==> EX! y. : ?f" fun_weaken_type: "[| ?f : ?A -> ?B; ?B <= ?D |] ==> ?f : ?A -> ?D" function_Union: "[| ALL x:?S. function(x); ALL x:?S. ALL y:?S. x <= y | y <= x |] ==> function(Union(?S))" if_P: "?P ==> if(?P, ?a, ?b) = ?a" if_cong: "[| ?P <-> ?Q; ?Q ==> ?a = ?c; ~ ?Q ==> ?b = ?d |] ==> if(?P, ?a, ?b) = if(?Q, ?c, ?d)" if_false: "if(False, ?a, ?b) = ?b" if_iff: "?a : if(?P, ?x, ?y) <-> ?P & ?a : ?x | ~ ?P & ?a : ?y" if_not_P: "~ ?P ==> if(?P, ?a, ?b) = ?b" if_true: "if(True, ?a, ?b) = ?a" if_type: "[| ?P ==> ?a : ?A; ~ ?P ==> ?b : ?A |] ==> if(?P, ?a, ?b) : ?A" imageE: "[| ?b : ?r `` ?A; !!x. [| : ?r; x : ?A |] ==> ?P |] ==> ?P" imageI: "[| : ?r; ?a : ?A |] ==> ?b : ?r `` ?A" image_0: "?r `` 0 = 0" image_Int_square: "?B <= ?A ==> (?r Int ?A * ?A) `` ?B = ?r `` ?B Int ?A" image_Int_square_subset: "(?r Int ?A * ?A) `` ?B <= ?r `` ?B Int ?A" image_Int_subset: "?r `` (?A Int ?B) <= ?r `` ?A Int ?r `` ?B" image_Un: "?r `` (?A Un ?B) = ?r `` ?A Un ?r `` ?B" image_fun: "[| ?f : Pi(?A, ?B); ?C <= ?A |] ==> ?f `` ?C = {?f ` x . x: ?C}" image_iff: "?b : ?r `` ?A <-> (EX x:?A. : ?r)" image_lam: "?C <= ?A ==> (lam x:?A. ?b(x)) `` ?C = {?b(x) . x: ?C}" image_mono: "[| ?r <= ?s; ?A <= ?B |] ==> ?r `` ?A <= ?s `` ?B" image_pair_mono: "[| !!x y. : ?r ==> : ?s; ?A <= ?B |] ==> ?r `` ?A <= ?s `` ?B" image_singleton_iff: "?b : ?r `` {?a} <-> : ?r" image_subset: "?r <= ?A * ?B ==> ?r `` ?C <= ?B" in_mono: "?A <= ?B ==> ?x : ?A --> ?x : ?B" lamD: " : (lam x:?A. ?b(x)) ==> ?c = ?b(?a)" lamE: "[| ?p : (lam x:?A. ?b(x)); !!x. [| x : ?A; ?p = |] ==> ?P |] ==> ?P" lamI: "?a : ?A ==> : (lam x:?A. ?b(x))" lam_cong: "[| ?A = ?A'; !!x. x : ?A' ==> ?b(x) = ?b'(x) |] ==> Lambda(?A, ?b) = Lambda(?A', ?b')" lam_funtype: "(lam x:?A. ?b(x)) : ?A -> {?b(x) . x: ?A}" lam_mono: "?A <= ?B ==> Lambda(?A, ?c) <= Lambda(?B, ?c)" lam_theI: "(!!x. x : ?A ==> EX! y. ?Q(x, y)) ==> EX f. ALL x:?A. ?Q(x, f ` x)" lam_type: "(!!x. x : ?A ==> ?b(x) : ?B(x)) ==> (lam x:?A. ?b(x)) : Pi(?A, ?B)" mem_asym: "[| ?a : ?b; ?b : ?a |] ==> ?P" mem_imp_not_eq: "?a : ?A ==> ?a ~= ?A" mem_irrefl: "?a : ?a ==> ?P" mem_not_refl: "?a ~: ?a" non_empty_family: "[| 0 ~: ?A; ?x : ?A |] ==> EX y. y : ?x" not_emptyE: "[| ?A ~= 0; !!x. x : ?A ==> ?R |] ==> ?R" not_emptyI: "?a : ?A ==> ?A ~= 0" pairing: "?c : Upair(?a, ?b) <-> ?c = ?a | ?c = ?b" prod_Int_distrib2: "?I * (?A Int ?B) = ?I * ?A Int ?I * ?B" prod_Un_distrib2: "?I * (?A Un ?B) = ?I * ?A Un ?I * ?B" rangeE: "[| ?b : range(?r); !!x. : ?r ==> ?P |] ==> ?P" rangeI: " : ?r ==> ?b : range(?r)" range_0: "range(0) = 0" range_Diff_subset: "range(?A) - range(?B) <= range(?A - ?B)" range_Int_subset: "range(?A Int ?B) <= range(?A) Int range(?B)" range_Un_eq: "range(?A Un ?B) = range(?A) Un range(?B)" range_cons: "range(cons(, ?r)) = cons(?b, range(?r))" range_converse: "range(converse(?r)) = domain(?r)" range_mono: "?r <= ?s ==> range(?r) <= range(?s)" range_of_fun: "?f : Pi(?A, ?B) ==> ?f : ?A -> range(?f)" range_of_prod: "?a : ?A ==> range(?A * ?B) = ?B" range_rel_subset: "?r <= ?A * ?C ==> range(?r) <= ?C" range_subset: "range(?A * ?B) <= ?B" range_subset_field: "range(?r) <= field(?r)" range_type: "[| : ?f; ?f : Pi(?A, ?B) |] ==> ?b : ?B(?a)" rel_Un: "[| ?r <= ?A * ?B; ?s <= ?C * ?D |] ==> ?r Un ?s <= (?A Un ?C) * (?B Un ?D)" rel_Union: "ALL x:?S. EX A B. x <= A * B ==> Union(?S) <= domain(Union(?S)) * range(Union(?S))" restrict: "?a : ?A ==> restrict(?f, ?A) ` ?a = ?f ` ?a" restrict_eqI: "[| ?A = ?B; !!x. x : ?B ==> ?f ` x = ?g ` x |] ==> restrict(?f, ?A) = restrict(?g, ?B)" restrict_lam_eq: "?A <= ?C ==> restrict(lam x:?C. ?b(x), ?A) = (lam x:?A. ?b(x))" restrict_subset: "[| ?f : Pi(?C, ?B); ?A <= ?C |] ==> restrict(?f, ?A) <= ?f" restrict_type: "(!!x. x : ?A ==> ?f ` x : ?B(x)) ==> restrict(?f, ?A) : Pi(?A, ?B)" restrict_type2: "[| ?f : Pi(?C, ?B); ?A <= ?C |] ==> restrict(?f, ?A) : Pi(?A, ?B)" rev_ballE: "[| ALL x:?A. ?P(x); ?x ~: ?A ==> ?Q; ?P(?x) ==> ?Q |] ==> ?Q" rev_bspec: "[| ?x : ?A; ALL x:?A. ?P(x) |] ==> ?P(?x)" rev_subsetD: "[| ?c : ?A; ?A <= ?B |] ==> ?c : ?B" separation: "?a : {x: ?A . ?P(x)} <-> ?a : ?A & ?P(?a)" setup_induction: "[| ?p : ?A; !!z. z : ?A ==> ?p = z --> ?R |] ==> ?R" singletonE: "[| ?a : {?b}; ?a = ?b ==> ?P |] ==> ?P" singletonI: "?a : {?a}" singleton_eq_iff: "{?a} = {?b} <-> ?a = ?b" singleton_fun: "{} : {?a} -> {?b}" singleton_iff: "?a : {?b} <-> ?a = ?b" singleton_subsetD: "{?a} <= ?C ==> ?a : ?C" singleton_subsetI: "?a : ?C ==> {?a} <= ?C" snd_conv: "snd() = ?b" snd_type: "?p : Sigma(?A, ?B) ==> snd(?p) : ?B(fst(?p))" split: "(%. ?c(x, y))() == ?c(?a, ?b)" splitD: "split(?R, ) ==> ?R(?a, ?b)" splitE: "[| split(?R, ?z); ?z : Sigma(?A, ?B); !!x y. [| ?z = ; ?R(x, y) |] ==> ?P |] ==> ?P" splitI: "?R(?a, ?b) ==> split(?R, )" split_type: "[| ?p : Sigma(?A, ?B); !!x y. [| x : ?A; y : ?B(x) |] ==> ?c(x, y) : ?C() |] ==> (%. ?c(x, y))(?p) : ?C(?p)" subsetCE: "[| ?A <= ?B; ?c ~: ?A ==> ?P; ?c : ?B ==> ?P |] ==> ?P" subsetD: "[| ?A <= ?B; ?c : ?A |] ==> ?c : ?B" subsetI: "(!!x. x : ?A ==> x : ?B) ==> ?A <= ?B" subset_Collect: "[| ?X <= ?A; !!z. z : ?X ==> ?P(z) |] ==> ?X <= Collect(?A, ?P)" subset_Int_iff: "?A <= ?B <-> ?A Int ?B = ?A" subset_Int_iff2: "?A <= ?B <-> ?B Int ?A = ?A" subset_Pow_Union: "?A <= Pow(Union(?A))" subset_UN_iff_eq: "?A <= (UN i:?I. ?B(i)) <-> ?A = (UN i:?I. ?A Int ?B(i))" subset_Un_iff: "?A <= ?B <-> ?A Un ?B = ?B" subset_Un_iff2: "?A <= ?B <-> ?B Un ?A = ?B" subset_consI: "?B <= cons(?a, ?B)" subset_cons_iff: "?C <= cons(?a, ?B) <-> ?C <= ?B | ?a : ?C & ?C - {?a} <= ?B" subset_empty_iff: "?A <= 0 <-> ?A = 0" subset_iff: "?A <= ?B <-> (ALL x. x : ?A --> x : ?B)" subset_refl: "?A <= ?A" subset_succI: "?i <= succ(?i)" subset_trans: "[| ?A <= ?B; ?B <= ?C |] ==> ?A <= ?C" succCI: "(?i ~: ?j ==> ?i = ?j) ==> ?i : succ(?j)" succE: "[| ?i : succ(?j); ?i = ?j ==> ?P; ?i : ?j ==> ?P |] ==> ?P" succI1: "?i : succ(?i)" succI2: "?i : ?j ==> ?i : succ(?j)" succ_iff: "?i : succ(?j) <-> ?i = ?j | ?i : ?j" succ_inject: "succ(?m) = succ(?n) ==> ?m = ?n" succ_inject_iff: "succ(?m) = succ(?n) <-> ?m = ?n" succ_neq_0: "succ(?n) = 0 ==> ?P" succ_not_0: "succ(?n) ~= 0" succ_subsetE: "[| succ(?i) <= ?j; [| ?i : ?j; ?i <= ?j |] ==> ?P |] ==> ?P" succ_subsetI: "[| ?i : ?j; ?i <= ?j |] ==> succ(?i) <= ?j" theI: "EX! x. ?P(x) ==> ?P(THE x. ?P(x))" theI2: "[| EX! x. ?P(x); !!x. ?P(x) ==> ?Q(x) |] ==> ?Q(THE x. ?P(x))" the_0: "~ (EX! x. ?P(x)) ==> (THE x. ?P(x)) = 0" the_equality: "[| ?P(?a); !!x. ?P(x) ==> x = ?a |] ==> (THE x. ?P(x)) = ?a" the_equality2: "[| EX! x. ?P(x); ?P(?a) |] ==> (THE x. ?P(x)) = ?a" triv_RepFun: "{x . x: ?A} = ?A" underD: "?a : ?r -`` {?b} ==> : ?r" underI: " : ?r ==> ?a : ?r -`` {?b}" vimageE: "[| ?a : ?r -`` ?B; !!x. [| : ?r; x : ?B |] ==> ?P |] ==> ?P" vimageI: "[| : ?r; ?b : ?B |] ==> ?a : ?r -`` ?B" vimage_0: "?r -`` 0 = 0" vimage_Int_square: "?B <= ?A ==> (?r Int ?A * ?A) -`` ?B = ?r -`` ?B Int ?A" vimage_Int_square_subset: "(?r Int ?A * ?A) -`` ?B <= ?r -`` ?B Int ?A" vimage_Int_subset: "?r -`` (?A Int ?B) <= ?r -`` ?A Int ?r -`` ?B" vimage_Un: "?r -`` (?A Un ?B) = ?r -`` ?A Un ?r -`` ?B" vimage_iff: "?a : ?r -`` ?B <-> (EX y:?B. : ?r)" vimage_mono: "[| ?r <= ?s; ?A <= ?B |] ==> ?r -`` ?A <= ?s -`` ?B" vimage_pair_mono: "[| !!x y. : ?r ==> : ?s; ?A <= ?B |] ==> ?r -`` ?A <= ?s -`` ?B" vimage_singleton_iff: "?a : ?r -`` {?b} <-> : ?r" vimage_subset: "?r <= ?A * ?B ==> ?r -`` ?C <= ?A" val it = () : unit -