---

Step * 2 of Lemma function-eq-transitivity-type-function


1. A : Type@i'
2. a : Base
3. b : Base
4. c : a = b ∈ type-function{i:l}(A)
5. f : Base@i
6. g : Base@i
7. h : Base@i
8. base-type-family{i:l}(A;x.a[x])
9. ∀[f,g:Base].  (function-eq(A;a@0.a[a@0];f;g) ∈ Type)
⊢ (function-eq(A;a@0.a[a@0];f;g) ⇒ function-eq(A;a@0.a[a@0];g;h) ⇒ function-eq(A;a@0.a[a@0];f;h))
= (function-eq(A;a.b[a];f;g) ⇒ function-eq(A;a.b[a];g;h) ⇒ function-eq(A;a.b[a];f;h))
∈ Type
BY
{ (InstLemma `function-eq_wf` [⌜A⌝;⌜b⌝]⋅ THEN Auto) }

1
.....antecedent..... 
1. A : Type@i'
2. a : Base
3. b : Base
4. c : a = b ∈ type-function{i:l}(A)
5. f : Base@i
6. g : Base@i
7. h : Base@i
8. base-type-family{i:l}(A;x.a[x])
9. ∀[f,g:Base].  (function-eq(A;a@0.a[a@0];f;g) ∈ Type)
⊢ base-type-family{i:l}(A;a.b[a])

2
1. A : Type@i'
2. a : Base
3. b : Base
4. c : a = b ∈ type-function{i:l}(A)
5. f : Base@i
6. g : Base@i
7. h : Base@i
8. base-type-family{i:l}(A;x.a[x])
9. ∀[f,g:Base].  (function-eq(A;a@0.a[a@0];f;g) ∈ Type)
10. ∀[f,g:Base].  (function-eq(A;a.b[a];f;g) ∈ Type)
⊢ (function-eq(A;a@0.a[a@0];f;g) ⇒ function-eq(A;a@0.a[a@0];g;h) ⇒ function-eq(A;a@0.a[a@0];f;h))
= (function-eq(A;a.b[a];f;g) ⇒ function-eq(A;a.b[a];g;h) ⇒ function-eq(A;a.b[a];f;h))
∈ Type

---

Latex:

---

Latex:

1.  A  :  Type@i'
2.  a  :  Base
3.  b  :  Base
4.  c  :  a  =  b
5.  f  :  Base@i
6.  g  :  Base@i
7.  h  :  Base@i
8.  base-type-family\{i:l\}(A;x.a[x])
9.  \mforall{}[f,g:Base].    (function-eq(A;a@0.a[a@0];f;g)  \mmember{}  Type)
\mvdash{}  (function-eq(A;a@0.a[a@0];f;g)  {}\mRightarrow{}  function-eq(A;a@0.a[a@0];g;h)  {}\mRightarrow{}  function-eq(A;a@0.a[a@0];f;h))
=  (function-eq(A;a.b[a];f;g)  {}\mRightarrow{}  function-eq(A;a.b[a];g;h)  {}\mRightarrow{}  function-eq(A;a.b[a];f;h))


By

---

Latex:
(InstLemma  `function-eq\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index