---

Step * of Lemma fix-corec-family-partial1

∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type]. ∀[A:Type].
  (∀[F:(P ⟶ Type) ⟶ P ⟶ Type]. ∀[f:(i:P ⟶ (corec-family(H) i) ⟶ partial(A))
                                      ⟶ i:P
                                      ⟶ (corec-family(H) i)
                                      ⟶ partial(A)].
     (fix(f) ∈ i:P ⟶ (corec-family(H) i) ⟶ partial(A))) supposing 
     (mono(A) and 
     value-type(A))
BY
{ (Auto
   THEN (ExtWith [`i'] [⌜Void ⟶ Void⌝]⋅ THENA Auto)
   THEN (ExtWith [`x'] [⌜Void ⟶ Void⌝]⋅ THENA Auto)
   THEN InstLemma `fixpoint-induction-bottom2` [⌜A⌝;⌜i:P ⟶ (corec-family(H) i) ⟶ partial(A)⌝;⌜λ2f.f i x⌝;⌜f⌝]⋅
   THEN Auto
   THEN RepeatFor 2 ((FunExt THEN Auto))
   THEN Subst' ⊥ i1 x1 ~ ⊥ 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[H:(P  {}\mrightarrow{}  Type)  {}\mrightarrow{}  P  {}\mrightarrow{}  Type].  \mforall{}[A:Type].
    (\mforall{}[F:(P  {}\mrightarrow{}  Type)  {}\mrightarrow{}  P  {}\mrightarrow{}  Type].  \mforall{}[f:(i:P  {}\mrightarrow{}  (corec-family(H)  i)  {}\mrightarrow{}  partial(A))
                                                                            {}\mrightarrow{}  i:P
                                                                            {}\mrightarrow{}  (corec-family(H)  i)
                                                                            {}\mrightarrow{}  partial(A)].
          (fix(f)  \mmember{}  i:P  {}\mrightarrow{}  (corec-family(H)  i)  {}\mrightarrow{}  partial(A)))  supposing 
          (mono(A)  and 
          value-type(A))


By

---

Latex:
(Auto
  THEN  (ExtWith  [`i']  [\mkleeneopen{}Void  {}\mrightarrow{}  Void\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (ExtWith  [`x']  [\mkleeneopen{}Void  {}\mrightarrow{}  Void\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstLemma  `fixpoint-induction-bottom2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}i:P  {}\mrightarrow{}  (corec-family(H)  i)  {}\mrightarrow{}  partial(A)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f.f 
                                                                                                                                                                                                    i 
                                                                                                                                                                                                    x\mkleeneclose{}
  ;\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  ((FunExt  THEN  Auto))
  THEN  Subst'  \mbot{}  i1  x1  \msim{}  \mbot{}  0
  THEN  Auto)

---

Home Index