proposition: Lemma Map2_map_law2'' : Map_law'' Map2_map1''.
proof: Proof. unfold Map_law'', Map2_map1'' in |- *. intros a1 a2 H; simpl in |- *; unfold Ext'' in |- *; intro b; simpl in |- *. apply pgcr; trivial. Qed.
imports: Relations