proposition: Lemma full_set_full : Equal (comp_map_map set_to_full full_to_set) (Id (full E)).
proof: Proof. simpl in |- *; auto with algebra. red in |- *. simpl in |- *; auto with algebra. intros x; try assumption. elim x. simpl in |- *; auto with algebra. intros subtype_elt' subtype_prf'; red in |- *. simpl in |- *; auto with algebra. Qed.
imports: Sets