proposition: Lemma tcreate_value_type : forall x (f:x->E) y, V (R y) (tcreate f) = f y.
proof: Proof. ir. uf tcreate. rw create_V_rewrite. assert (inc (R y) x). ap R_inc. apply Yy_if with H. rw B_back. tv. ap R_inc. Qed.
imports: set_theory