proposition: Lemma RenBindersSpec : forall {G : CFGV} (vc : VarSym G), ( forall (s : GSym G) (nt : Term s), True) * ( forall (s : GSym G) (pt : Pattern s) (lvAvoid : lVars vc), let ptr := (pRenBinders lvAvoid pt) in no_repeats (pBndngVars vc ptr) # disjoint (pBndngVars vc ptr) lvAvoid ) * ( forall (l : list (bool # GSym G)) (m : Mixture l) (lvAvoid : lVars vc), let mr := (mRenBinders lvAvoid m) in no_repeats (mBndngVars vc mr) # disjoint (mBndngVars vc mr) lvAvoid ).
proof: Proof. intros. GInduction; cpx;[|]. - Case "pvleaf". allsimpl. intros. dands; rewrite DeqSym; ddeq; subst; allsimpl; try constructor; cpx. repeat (disjoint_reasoning). apply vFreshVarSpec. - Case "mpcons". introns Hyp. allsimpl. intros. specialize (Hyp0 (lvAvoid ++ (pBndngVars vc (pRenBinders lvAvoid ph)))). specialize (Hyp lvAvoid ). allrw no_repeats_app. repnd; dands;cpx; repeat (disjoint_reasoning); cpx. Qed.
imports: AlphaEqProps Omega