fact: Fixpoint tse_int (S T:CSetoid) (r:S) (e:tot_set_exp S T) {struct e} : T := match e with | tse_var _ => r | tse_fun _ T1 T2 f e0 => f (tse_int S T1 r e0) | tse_bfun _ T1 T2 T3 f e1 e2 => f (tse_int S T1 r e1) (tse_int S T2 r e2) | tse_con _ T t => t end.
imports: CoRN.algebra.CSetoidFun