proposition: Lemma rew_pair A (P Q : A->Type) x1 x2 (y1:P x1) (y2:Q x1) (H:x1=x2) : (rew H in y1, rew H in y2) = rew [fun x => (P x * Q x)%type] H in (y1,y2).
proof: Proof. destruct H. reflexivity. Defined.
imports: Notations Ltac Logic