proposition: Lemma replacement_lemma : forall (T:CSetoid) (e:part_set_exp T) (r1 r2 t1:T), (r1[=]r2) -> pse_int r1 e t1 -> my_sigT T (pse_int r2 e).
proof: Proof. intros T e r1 r2 t1 H H0. elim H0; clear H0 e t1. exists r2. apply pse_int_var. intros F e a1 Ha1 IH. elim IH; intros a2 Ha2. exists (F a2); apply pse_int_uop with (1 := Ha2). intros F ea a1 eb b1 Ha1 IHa Hb1 IHb. elim IHa; intros a2 Ha2. elim IHb; intros b2 Hb2. exists (F a2 b2); apply pse_int_bop with (1 := Ha2) (2 := Hb2). intros F e a1 Ha1 IH Da1. elim IH; intros a2 Ha2. assert (Da2 := cspf_dom_wd T T F a1 a2 Da1 (pse_int_wd H Ha1 Ha2)). exists (F a2 Da2). apply pse_int_pop with (1 := Ha2). intro t; exists t; apply pse_int_con. Defined.
imports: CoRN.algebra.CSetoidFun