proposition: Lemma enc_sol_T theta x y z: (enc_sol theta (G x y z)) = T (theta y) (theta x).
proof: Proof. unfold enc_sol. destruct partition_F_G as [[x' ?]|[((x',y'),z') ?]]. - exfalso; eapply disjoint_F_G; (eauto 2). - now eapply G_injective in y0 as (-> & -> & ->). Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)