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