proposition: Lemma prod2_equiv : forall A1 A2 (E1:binary A1) (E2:binary A2), equiv E1 -> equiv E2 -> equiv (prod2 E1 E2).
proof: Proof. Proof using. introv [R1 S1 T1] [R2 S2 T2]. constructor. { intros [x1 x2]. simple*. } { intros [x1 x2] [y1 y2]. simple*. } { intros [x1 x2] [y1 y2] [z1 z2]. simple*. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)