proposition: Lemma tse_int_wd : forall (S T:CSetoid) (r1 r2:S), (r1[=]r2) -> forall e:tot_set_exp S T, tse_int S T r1 e[=]tse_int S T r2 e.
proof: Proof. intros S T r1 r2 h. induction e; simpl in |- *. exact h. apply csf_wd; assumption. apply csbf_wd; assumption. apply eq_reflexive. Qed.
imports: CoRN.algebra.CSetoidFun