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: Relations