proposition: Lemma tSwapBndngVarsDisjoint : forall {G : CFGV} {vc : VarSym G}, (forall (s : GSym G) (ta : Term s) (la lb : list (vType vc)) (lvA : list (vType vc)), disjoint (tBndngVarsDeep vc ta) lvA -> disjoint lb (lvA++ (tAllVars ta)) -> length la = length lb -> no_repeats lb -> disjoint la lb -> disjoint (tBndngVarsDeep vc (tSwap ta (combine la lb))) lvA).
proof: Proof. introv Ha Hb Hc Hd He. apply (tcase swapCommonBinders); autorewrite with fast; cpx. unfold lvKeep. rewrite lKeepDisjoint; cpx. disjoint_reasoning. Qed.
imports: Swap AssociationList Eqdep_dec