proposition: Lemma SU_H10 E: SOU ag 2 (H10_to_SOU E) -> H10 E.
proof: Proof. rewrite SOU_NSOU; (eauto 2). intros (Delta & sigma & T & EQ & N). exists (decode_subst sigma N). intros e H; pose (Q := eqs e). assert (forall p, p ∈ Q -> sigma • fst p ≡ sigma • snd p) as EQs; [|clear EQ]. - intros [s t] G. eapply EQ. eapply in_Equations. eauto. - destruct e; econstructor; cbn in Q, EQs. all: specialize (EQs (varEQ x)) as EQx; mp EQx; intuition idtac; eapply backward_vars in EQx as [n EQx]; (eauto 2). 2 - 3: specialize (EQs (varEQ y)) as EQy; mp EQy; intuition idtac; eapply backward_vars in EQy as [m EQy]; (eauto 2). 2 - 3: specialize (EQs (varEQ z)) as EQz; mp EQz; intuition idtac; eapply backward_vars in EQz as [p EQz]; (eauto 2). all: repeat (erewrite decode_subst_encodes;[|eauto]). + eapply backward_consts; (eauto 4). + eapply backward_add; (eauto 1); eapply EQs; (eauto 5). + eapply backward_mult; (eauto 1); eapply EQs; intuition idtac. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)