fact: Fixpoint forget (t:T) (e:part_set_xexp t) {struct e} : part_set_exp := match e with | psxe_var => pse_var | @psxe_uop F t0 e0 => pse_uop F (forget e0) | @psxe_bop F t1 t2 e1 e2 => pse_bop F (forget e1) (forget e2) | @psxe_pop F t0 H e0 => pse_pop F (forget e0) | @psxe_con t => pse_con t end.
imports: CoRN.algebra.CSetoidFun