proposition: Lemma pse_int_ext : forall (e:part_set_exp) (t t':T), pse_int e t -> pse_int e t' -> t[=]t'.
proof: Proof. simple induction e; clear e. intros t t' h h0. rewrite (pse_int_var_inv h). rewrite (pse_int_var_inv h0). apply eq_reflexive. intros F e IH t t' h h0. inversion_clear h; inversion_clear h0. apply csf_wd; apply IH; assumption. intros F e1 IH1 e2 IH2 t t' h h0. inversion_clear h; inversion_clear h0. apply csbf_wd; [ apply IH1 | apply IH2 ]; assumption. intros F e IH t t' h h0. inversion_clear h; inversion_clear h0. apply cspf_wd; apply IH; assumption. intros c t t' h h0. rewrite (pse_int_con_inv h). rewrite (pse_int_con_inv h0). apply eq_reflexive. Qed.
imports: CoRN.algebra.CSetoidFun