proposition: Lemma mkRestrPainting_step_computes {n} {C: νType n} {q r} {Hq: q.+2 <= n.+1} {Hrq: r.+2 <= q.+2} {ε: arity} {D E} {d: (mkFrame r).(frame) _ D} {c}: mkRestrPainting (Hpq := ↓ Hrq) (Hq := Hq) (ε := ε) E d c = match (rew [id] mkpainting_computes in c) with | (l; c) => rew <- [id] C.(eqPaintingSp) in (mkRestrLayer d l; mkRestrPainting (Hpq := Hrq) E (d; l) c) end.
proof: Proof. unfold mkRestrPainting; now rewrite le_induction'_step_computes. Qed.
imports: Logic.FunctionalExtensionality Bonak(Notation) Bonak(RewLemmas) Bonak(HSet) Bonak(LeYoneda)