fact: Definition mkRestrPainting {n} {C: νType n} {p q} {Hpq: p.+1 <= q.+1} {Hq: q.+1 <= n.+1} {ε: arity} {D} (E: (mkFrame n.+1).(frame) (♢ _) D -> HSet) (d: (mkFrame p).(frame) (↓ (Hpq ↕ Hq)) D) (Painting: mkpainting (Hp := ↓ (Hpq ↕ Hq)) E d): mkPaintingPrev.(painting') ((mkFrame p).(restrFrame) Hq ε d).
imports: Logic.FunctionalExtensionality Bonak(Notation) Bonak(RewLemmas) Bonak(HSet) Bonak(LeYoneda)