proposition: Lemma map_subst_app {A B} {x y} {𝛉: A} (H: x = y :> B) (P: A -> B -> Type) (f: forall 𝛉, P 𝛉 x): rew [P 𝛉] H in f 𝛉 = (rew [fun x => forall 𝛉, P 𝛉 x] H in f) 𝛉.
proof: Proof. now destruct H. Defined.
imports: Bonak(Notation)