proposition: Lemma SSubstAuxTrivial : ( (forall (s : GSym G) (t : Term s) (sub : SSubstitution vc), disjoint (tfreevars vc t) (ALDom sub) -> tSSubstAux t sub = t) * (forall (s : GSym G) (pt : Pattern s) (sub : SSubstitution vc), disjoint (pfreevars vc pt) (ALDom sub) -> pSSubstAux pt sub = pt) * (forall (l : list (bool # GSym G)) (m : Mixture l) (sub : SSubstitution vc) (llva : list (list (vType vc))), disjoint (mfreevars vc m llva) (ALDom sub) -> mSSubstAux m llva sub = m)).
proof: Proof. intros. apply GInduction; auto;[| | | | |]; try (intros; simpl; f_equal; f_equal; auto; fail); [| |]; try( (Case "mtcons" || Case "mpcons"); introv Hp Hm Hdis; allsimpl; destruct llva; allsimpl; disjoint_reasoning; f_equal; auto;[]; f_equal; auto; apply Hp; unfold SubFilter; rewrite <- ALDomFilterCommute; unfold subtractv in Hdis0; apply disjoint_diff_l; auto; fail);[]. introv Hdis. simpl. rename vc0 into vcc. destruct_head_match; auto;[]. subst vcc. simpl. rw ALFindDef2Same. unfold ALFindDef2. destruct_head_match; auto;[]. provefalse. destruct s; auto. allsimpl. rewrite DeqTrue in Hdis. allsimpl. disjoint_reasoning. apply Hdis. apply ALInEta in l. repnd; auto. Qed.
imports: Term AssociationList