proposition: Theorem rew_permute A (P Q: A -> Type) (x y: A) (H: forall z, Q z = P z) (H': x = y) (a: P x) : rew <- [id] H y in rew H' in a = rew [Q] H' in rew <- [id] H x in a.
proof: Proof. now destruct H'. Qed.
imports: Bonak(Notation)