---

Step * of Lemma corec-sub-family

∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type].  H corec-family(H) ⊆ corec-family(H) supposing family-monotone{i:l}(P;H)
BY
{ (Auto
   THEN RW (AddrC [3] UnfoldTopAbC) 0
   THEN BLemma `sub-isect-family`⋅
   THEN Auto
   THEN (RWO "fun_exp_unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN (BackThruSomeHyp' ORELSE (D 0 THEN Reduce 0 THEN Auto))
   THEN RW (AddrC [2] UnfoldTopAbC) 0
   THEN D 0
   THEN RepUR ``isect-family`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[H:(P  {}\mrightarrow{}  Type)  {}\mrightarrow{}  P  {}\mrightarrow{}  Type].
    H  corec-family(H)  \msubseteq{}  corec-family(H)  supposing  family-monotone\{i:l\}(P;H)


By

---

Latex:
(Auto
  THEN  RW  (AddrC  [3]  UnfoldTopAbC)  0
  THEN  BLemma  `sub-isect-family`\mcdot{}
  THEN  Auto
  THEN  (RWO  "fun\_exp\_unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  (BackThruSomeHyp'  ORELSE  (D  0  THEN  Reduce  0  THEN  Auto))
  THEN  RW  (AddrC  [2]  UnfoldTopAbC)  0
  THEN  D  0
  THEN  RepUR  ``isect-family``  0
  THEN  Auto)

---

Home Index