---

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

.....wf..... 
1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. a : A
4. b : A
5. L : (a:A × b:A × ((R a b) ∨ (R b a))) List
6. rel_path(A;L;a;b) ∧ 0 < ||L||
7. L1 : (a:A × b:A × ((R a b) ∨ (R b a))) List
⊢ istype(rel_path(A;L1;b;a) ∧ 0 < ||L1||)
BY
{ (InstLemma `rel_path_wf` [⌜A⌝;⌜λ2a b.(R a b) ∨ (R b a)⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  A  :  Type
2.  R  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  a  :  A
4.  b  :  A
5.  L  :  (a:A  \mtimes{}  b:A  \mtimes{}  ((R  a  b)  \mvee{}  (R  b  a)))  List
6.  rel\_path(A;L;a;b)  \mwedge{}  0  <  ||L||
7.  L1  :  (a:A  \mtimes{}  b:A  \mtimes{}  ((R  a  b)  \mvee{}  (R  b  a)))  List
\mvdash{}  istype(rel\_path(A;L1;b;a)  \mwedge{}  0  <  ||L1||)


By

---

Latex:
(InstLemma  `rel\_path\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}a  b.(R  a  b)  \mvee{}  (R  b  a)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index