proposition: Lemma enc_sol_encodes theta h: encodes (enc_sol theta (F h)) (theta h).
proof: Proof. unfold enc_sol. destruct partition_F_G as [[x ?]|[((x,y),z) ?]]. - eapply F_injective in e as ->. intros t delta. unfold gf. cbn; rewrite stepBeta; asimpl; (eauto 2). - exfalso; eapply disjoint_F_G; (eauto 2). Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)