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