proposition: Lemma create_like : forall f g t, like (create f g t).
proof: Proof. ir. uf like. ap create_extensionality. rww source_create. rww target_create. ir. rww ntrans_create. rwi source_create H. am. Qed.
imports: Arith functor