proposition: Lemma subsetAlbindersDeep: forall {mp} (ma : Mixture mp) llb, subset (albindersDeep (MakeAbstractions vc ma llb)) ((mBndngVarsDeep vc ma) ++ flatten llb).
proof: Proof. induction ma; cpx; destruct llb; allsimpl; autorewrite with fast in *. - apply subset_app_lr; eauto. pose proof (IHma []); autorewrite with fast in *; cpx. - rw <- app_assoc. rw <- app_assoc. apply subset_app_lr; eauto. eapply subset_trans; [|apply subsetAppEauto]. rewrite <- app_assoc. apply subset_app_lr; eauto. eapply subset_trans; [cpx|apply subsetAppEauto]. - apply subset_app_lr; eauto. pose proof (IHma []); autorewrite with fast in *; cpx. - rw <- app_assoc. rw <- app_assoc. apply subset_app_lr; eauto. eapply subset_trans; [|apply subsetAppEauto]. rewrite <- app_assoc. apply subset_app_lr; eauto. eapply subset_trans; [cpx|apply subsetAppEauto]. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux