proposition: Lemma IM_lift_pr : forall (a : E) (f : a -> E) (x : IM f), f (IM_lift x) = R x.
proof: Proof. ir. assert (exists y : a, f y = R x). ap IM_exists. ap R_inc. uf IM_lift. set (K := ex_ind (fun (x0 : a) (_ : (fun u : a => f u = R x) x0) => nonemptyT_intro x0) (IM_exists (R_inc x))) in *. pose (chooseT_pr K H). am. Qed.
imports: tactics