proposition: Lemma mkRestrPainting_base_computes {n} {C: νType n} {p} {Hp: p.+1 <= n.+1} {ε: arity} {D E} {d: (mkFrame p).(frame) _ D} {c}: mkRestrPainting (Hq := Hp) E d c = match (rew [id] mkpainting_computes in c) with | (l; _) => l ε end.
proof: Proof. unfold mkRestrPainting; now rewrite le_induction'_base_computes. Qed.
imports: Logic.FunctionalExtensionality Bonak(Notation) Bonak(RewLemmas) Bonak(HSet) Bonak(LeYoneda)