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