---

Step * 2 of Lemma inv_funs-iff


1. A : Type
2. B : Type
3. f : A ⟶ B
4. g : B ⟶ A
5. (g o f) = (λx.x) ∈ (A ⟶ A)
6. (f o g) = (λx.x) ∈ (B ⟶ B)
7. b : B
⊢ (f (g b)) = b ∈ B
BY
{ (Subst ⌜f (g b) ~ (f o g) b⌝ 0⋅
   THEN Try (Complete ((Reduce 0 THEN Auto)))
   THEN HypSubst (-2) 0
   THEN Reduce 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  g  :  B  {}\mrightarrow{}  A
5.  (g  o  f)  =  (\mlambda{}x.x)
6.  (f  o  g)  =  (\mlambda{}x.x)
7.  b  :  B
\mvdash{}  (f  (g  b))  =  b


By

---

Latex:
(Subst  \mkleeneopen{}f  (g  b)  \msim{}  (f  o  g)  b\mkleeneclose{}  0\mcdot{}
  THEN  Try  (Complete  ((Reduce  0  THEN  Auto)))
  THEN  HypSubst  (-2)  0
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index