proposition: Theorem renBindersSameLength: forall {G : CFGV} {vc : VarSym G}, ( forall (s : GSym G) (nt : Term s), True) * ( forall (s : GSym G) (pt : Pattern s) (lvA : lVars vc), length (pBndngVars vc pt) = length (pBndngVars vc (pRenBinders lvA pt)) ) * ( forall (l : list (bool # GSym G)) (m : Mixture l) (lvA : lVars vc) (nn : nat), length (getBVarsNth vc m nn) = length (getBVarsNth vc (mRenBinders lvA m) nn) ).
proof: Proof. intros. GInduction; allsimpl; introns Hyp; intros; cpx; [ | | | ]. - Case "pvleaf". rewrite DeqSym. symmetry. rewrite DeqSym. ddeq; subst; sp. - Case "pnode". simpl. simpl pBndngVars. rewrite mBndngVarsAsNth. rewrite mBndngVarsAsNth. rewrite len_flat_map. rewrite len_flat_map. f_equal. apply eq_maps. cpx. - simpl. destruct nn; cpx. - simpl. destruct nn; cpx. Qed.
imports: AlphaEqProps Omega