Step
*
1
of Lemma
image-per-symmetric
.....antecedent.....
1. A : Type
2. f : Base
3. a : Base
4. b : Base
5. TC(λx,y. ∃a,b:Base. ((a = b ∈ A) ∧ (x ~ f a) ∧ (y ~ f b))) a b
⊢ Sym(Base;x,y.(λx,y. ∃a,b:Base. ((a = b ∈ A) ∧ (x ~ f a) ∧ (y ~ f b))) x y)
BY
{ ((D 0 THEN Reduce 0) THEN Auto) }
Latex:
Latex:
.....antecedent.....
1. A : Type
2. f : Base
3. a : Base
4. b : Base
5. TC(\mlambda{}x,y. \mexists{}a,b:Base. ((a = b) \mwedge{} (x \msim{} f a) \mwedge{} (y \msim{} f b))) a b
\mvdash{} Sym(Base;x,y.(\mlambda{}x,y. \mexists{}a,b:Base. ((a = b) \mwedge{} (x \msim{} f a) \mwedge{} (y \msim{} f b))) x y)
By
Latex:
((D 0 THEN Reduce 0) THEN Auto)
Home
Index