proposition: Lemma extract_correct : forall (t:T) (e:part_set_xexp t), pse_int (forget e) t.
proof: Proof. simple induction e; clear e t; simpl in |- *. exact pse_int_var. intros F t e h. apply pse_int_uop; exact h. intros F t1 t2 e1 h1 e2 h2. apply pse_int_bop with (1 := h1) (2 := h2). intros F t Ht e h. apply pse_int_pop; exact h. exact pse_int_con. Defined.
imports: CoRN.algebra.CSetoidFun