fact: Definition mkCohPainting_step {n} {C: νType n} {p q r} {Hpr: p.+3 <= r.+3} {Hrq: r.+3 <= q.+3} {Hq: q.+3 <= n.+1} {ε ω: arity} {D} {E: (mkFrame n.+1).(frame) (♢ _) D -> HSet} {d: (mkFrame p).(frame) (↓ ↓ (↓ Hpr ↕ Hrq ↕ Hq)) D} {c: mkpainting E d} {IHP: forall (d: (mkFrame p.+1).(frame) (↓ ↓ (Hpr ↕ Hrq ↕ Hq)) D) (c: mkpainting E d), mkCohPaintingHyp p.+1 Hpr (ε := ε) (ω := ω) d c}: mkCohPaintingHyp p (↓ Hpr) (ε := ε) (ω := ω) d c.
imports: Logic.FunctionalExtensionality Bonak(Notation) Bonak(RewLemmas) Bonak(HSet) Bonak(LeYoneda)