proposition: Lemma Prf_map2_cong : Map2_cong_law Ap2.
proof: Proof. unfold Map2_cong_law in |- *; intros a1 a2 b1 b2 H1 H2. apply Trans with (Ap2 a2 b1). apply (Prf_map2_congr b1 H1). apply (Prf_map2_congl a2 H2). Qed.
imports: SetoidPROD