---

Step * 2 1 1 1 1 2 1 1 2 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) ∈ ℙ)
⊢ ∀aaaa:a:A × b:A × ((R a b) ∨ (R b a)). ∀LLLL:(a:A × b:A × ((R a b) ∨ (R b a))) List.
    ((∀a,b:A.
        (rel_path(A;LLLL;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>;LLLL));b;a)))
    ⇒ (∀a,b:A.
          (rel_path(A;[aaaa / LLLL];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>;[aaaa / LLLL]));b;a))))
BY
{ ((D 0 THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN Reduce 0
   THEN RepeatFor 4 ((D 0 THENA Auto))
   THEN RepUR ``rel_path`` 0
   THEN Fold `rel_path` 0
   THEN (D 0 THENA Auto)) }

1
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) ∈ ℙ)
5. a : A
6. b : A
7. a2 : (R a b) ∨ (R b a)
8. LLLL : (a:A × b:A × ((R a b) ∨ (R b a))) List
9. ∀a,b:A.
     (rel_path(A;LLLL;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>;LLLL));b;a))
10. a@0 : A
11. b@0 : A
12. (a = a@0 ∈ A) ∧ rel_path(A;LLLL;b;b@0)
⊢ 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>;LLLL))
@ [<b, a, case a2 of inl(x) => inr x  | inr(x) => inl x>];b@0;a@0)

---

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{}aaaa:a:A  \mtimes{}  b:A  \mtimes{}  ((R  a  b)  \mvee{}  (R  b  a)).  \mforall{}LLLL:(a:A  \mtimes{}  b:A  \mtimes{}  ((R  a  b)  \mvee{}  (R  b  a)))  List.
        ((\mforall{}a,b:A.
                (rel\_path(A;LLLL;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>LLLL));b;a)))
        {}\mRightarrow{}  (\mforall{}a,b:A.
                    (rel\_path(A;[aaaa  /  LLLL];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>
                                                                [aaaa  /  LLLL]));b;a))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  Reduce  0
  THEN  RepeatFor  4  ((D  0  THENA  Auto))
  THEN  RepUR  ``rel\_path``  0
  THEN  Fold  `rel\_path`  0
  THEN  (D  0  THENA  Auto))

---

Home Index