---

Step * 2 1 1 1 1 2 1 1 1 of Lemma least-equiv-is-equiv-1

.....antecedent..... 
1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. L : (a:A × b:A × ((R a b) ∨ (R b a))) List
4. ∀[x,y:A]. ∀[L:(a:A × b:A × ((R a b) ∨ (R b a))) List].  (rel_path(A;L;x;y) ∈ ℙ)
⊢ ∀a,b:A.
    (rel_path(A;[];a;b) ⇒ rel_path(A;rev(map(λt.let a,b,r = t in <b, a, case r of inl(x) => inr x  | inr(x) => inl x>;[\000C]));b;a))
BY
{ (RepUR ``rel_path`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  A  :  Type
2.  R  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  L  :  (a:A  \mtimes{}  b:A  \mtimes{}  ((R  a  b)  \mvee{}  (R  b  a)))  List
4.  \mforall{}[x,y:A].  \mforall{}[L:(a:A  \mtimes{}  b:A  \mtimes{}  ((R  a  b)  \mvee{}  (R  b  a)))  List].    (rel\_path(A;L;x;y)  \mmember{}  \mBbbP{})
\mvdash{}  \mforall{}a,b:A.
        (rel\_path(A;[];a;b)
        {}\mRightarrow{}  rel\_path(A;rev(map(\mlambda{}t.let  a,b,r  =  t  in 
                                                          <b,  a,  case  r  of  inl(x)  =>  inr  x    |  inr(x)  =>  inl  x>[]));b;a))


By

---

Latex:
(RepUR  ``rel\_path``  0  THEN  Auto)

---

Home Index