proposition: Lemma typing_forward sigma: (sigma ⊢⁺ₑ E) -> [] ⊩(2) enc_sol sigma : Gamma__deq E.
proof: Proof. eauto; intros ????; unfold enc_sol. destruct partition_F_G as [[]|[((x & y) & z) ?]]; subst. + eapply nth_Gamma__deq_F in H0 as ->. eapply gf_typing. + eapply nth_Gamma__deq_G in H0 as ->. eapply GT_typing. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)