proposition: Lemma map_couple_proj_prop : Equal (map_couple map_proj1 map_proj2) f.
proof: Proof. simpl in |- *. red in |- *. unfold map_proj1, map_proj2 in |- *; simpl in |- *. unfold app_rel, cart_eq in |- *; intuition. Qed.
imports: Sets