proposition: Lemma tcreate_value_inc : forall x (f:x->E) y (hyp : inc y x), V y (tcreate f) = f (B hyp).
proof: Proof. ir. assert (y = R (B hyp)). rww B_eq. transitivity (V (R (B hyp)) (tcreate f)). wr H. tv. ap tcreate_value_type. Qed.
imports: set_theory