proposition: Lemma mkpainting_computes {n p} {C: νType n} {Hp: p.+1 <= n.+1} {D} {E: (mkFrame n.+1).(frame) (♢ _) D -> HSet} {d}: mkpainting (Hp := ↓ Hp) E d = {l : mkLayer & mkpainting (Hp := Hp) E (d; l)} :> Type.
proof: Proof. unfold mkpainting; now rewrite le_induction_step_computes. Qed.
imports: Logic.FunctionalExtensionality Bonak(Notation) Bonak(RewLemmas) Bonak(HSet) Bonak(LeYoneda)