---

Step * of Lemma eu-seg-congruent-iff-length

∀e:EuclideanPlane. ∀[s,t:Segment].  uiff(s ≡ t;|s| = |t| ∈ {p:Point| O_X_p} )
BY
{ (Auto THEN Try ((EqTypeCD THEN Auto))) }

1
1. e : EuclideanPlane@i'
2. s : Segment
3. t : Segment
4. s ≡ t
⊢ |s| = |t| ∈ Point

2
1. e : EuclideanPlane@i'
2. [s] : Segment
3. [t] : Segment
4. |s| = |t| ∈ {p:Point| O_X_p} 
⊢ s ≡ t

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[s,t:Segment].    uiff(s  \mequiv{}  t;|s|  =  |t|)


By

---

Latex:
(Auto  THEN  Try  ((EqTypeCD  THEN  Auto)))

---

Home Index