proposition: Lemma canonical2_substrate r r': fam_of_substrates (variantLc r r') = variantLc (substrate r) (substrate r').
proof: Proof. rewrite /fam_of_substrates /variantLc. apply: fgraph_exten; aww. by move=> x xtp; rewrite LgV //; try_lvariant xtp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)