proposition: Corollary SSubstAuxNilNoChange : ( (forall (s : GSym G) (t : Term s), @tSSubstAux _ vc _ t [] = t) * (forall (s : GSym G) (pt : Pattern s), @pSSubstAux _ vc _ pt [] = pt) * (forall (l : list (bool # GSym G)) (m : Mixture l) (llva : list (list (vType vc))), mSSubstAux m llva [] = m)).
proof: Proof. pose proof SSubstAuxTrivial. repnd. dands; intros; auto; apply_hyp; allsimpl; disjoint_reasoning. Qed.
imports: Term AssociationList