---

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


1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. L : (a:A × b:A × ((R a b) ∨ (R b a))) List
⊢ ∀a,b:A.
    (rel_path(A;L;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>;L)\000C);b;a))
BY
{ ((InstLemma `rel_path_wf` [⌜A⌝;⌜λ2a b.(R a b) ∨ (R b a)⌝]⋅ THENA Auto)
   THEN InstLemma `list_induction` [⌜a:A × b:A × ((R a b) ∨ (R b a))⌝;⌜λ2L.∀a,b:A.
                                                                             (rel_path(A;L;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>;L));b;a))⌝
   ;⌜L⌝]⋅
   THEN Try (Complete (Auto))) }

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))

2
.....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))))

---

Latex:

---

Latex:

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
\mvdash{}  \mforall{}a,b:A.
        (rel\_path(A;L;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>L));b;a))


By

---

Latex:
((InstLemma  `rel\_path\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}a  b.(R  a  b)  \mvee{}  (R  b  a)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstLemma  `list\_induction`  [\mkleeneopen{}a:A  \mtimes{}  b:A  \mtimes{}  ((R  a  b)  \mvee{}  (R  b  a))\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}L.\mforall{}a,b:A.
                (rel\_path(A;L;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>L));b;a))\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}
  ]\mcdot{}
  THEN  Try  (Complete  (Auto)))

---

Home Index