proposition: Lemma swapDisjChain : forall (vsa vs vsb : list vcType), length vs = length vsa -> length vs = length vsb -> no_repeats vs -> no_repeats vsb -> (forall (gs : GSym G) (t : Term gs), disjoint vs (vsa ++ vsb ++ (tAllVars t)) -> disjoint vsb (vsa ++ tAllVars t) -> tSwap t ((combine vsa vs) ++ (combine vs vsb)) = tSwap t (combine vsa vsb)) * (forall (gs : GSym G) (t : Pattern gs), disjoint vs (vsa ++ vsb ++ (pAllVars t)) -> disjoint vsb (vsa ++ pAllVars t) -> pSwap t ((combine vsa vs) ++ (combine vs vsb)) = pSwap t (combine vsa vsb)) * (forall (lgs : MixtureParam) (m : Mixture lgs) , disjoint vs (vsa ++ vsb ++ (mAllVars m)) -> disjoint vsb (vsa ++ mAllVars m) -> mSwap m ((combine vsa vs) ++ (combine vs vsb)) = mSwap m (combine vsa vsb)).
proof: Proof. introv Hlena Hlenb Hnr Hnrb. apply GInduction; auto; introns Hdis; allsimpl. - Case "vleaf". simpl. f_equal. rewrite DeqSym. symmetry. rewrite DeqSym. destruct_head_match; cpx. subst. simpl. symmetry. apply swapVarDisjChain; auto; repeat(disjoint_reasoning); allsimpl; allrewrite (@DeqTrue (VarSym G)); allsimpl; repeat(disjoint_reasoning). - Case "pnode". rw Hdis; simpl; auto. - Case "pvleaf". simpl. f_equal. rewrite DeqSym. symmetry. rewrite DeqSym. destruct_head_match; cpx. subst. simpl. symmetry. apply swapVarDisjChain; auto; repeat(disjoint_reasoning); allsimpl; allrewrite (@DeqTrue (VarSym G)); allsimpl; repeat(disjoint_reasoning). - rw Hdis; simpl; auto. - rw Hdis; simpl; auto. - f_equal. + apply Hdis; repeat(disjoint_reasoning). + apply Hdis0; repeat(disjoint_reasoning). - f_equal. + apply Hdis; repeat(disjoint_reasoning). + apply Hdis0; repeat(disjoint_reasoning). Qed.
imports: Swap AssociationList Eqdep_dec