proposition: Lemma left_vident : forall a, axioms a -> vcompose (vident (target a)) a = a.
proof: Proof. ir. ap axioms_extensionality. rww vcompose_axioms. nw. rww vident_axioms. nw. nw. am. nw. nw. ir. rwi osource_vcompose H0. nw'. cw. fw. nw. nw. nw. nw. Qed.
imports: Arith functor