proposition: Lemma length_pRhsAugIsPat : forall {G : CFGV} (p : TermProd G), length (tpRhsAugIsPat p) = length ((snd (tpLhsRhs G p))).
proof: Proof. intros. simpl. unfold tpRhsAugIsPat, prhsIsBound , tpRhsSym. rewrite combine_length. autorewrite with fast. rewrite min_eq; refl. Qed.
imports: GVariables