proposition: Lemma variantLc_comp a b f: variantLc (f a) (f b) = Lg (domain (variantLc a b))(fun z => f (Vg (variantLc a b) z)).
proof: Proof. apply: fgraph_exten;aww. move=> x xtp; try_lvariant xtp; rewrite LgV; aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)