---

Step * 1 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. a : A
⊢ (g (f a)) = a ∈ A
BY
{ (Subst ⌜g (f a) ~ (g o f) a⌝ 0⋅
   THEN Try (Complete ((Reduce 0 THEN Auto)))
   THEN HypSubst (-3) 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.  a  :  A
\mvdash{}  (g  (f  a))  =  a


By

---

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

---

Home Index