proposition: Lemma SU_NSU X I: SU X I <-> NSU I.
proof: Proof. split; intros (Delta & sigma & H1 & H2); [| exists Delta; exists sigma; intuition]. eapply normalise_subst in H1 as (tau & H5 & H6 & H7). pose (theta x := if nth (@Gammaᵤ' _ I) x then tau x else var x). exists Delta. exists theta. intuition idtac. + intros ???; unfold theta; rewrite H; eapply H7; eauto. + rewrite subst_pointwise_equiv with (sigma := theta) (tau := sigma). rewrite subst_pointwise_equiv with (sigma := theta) (tau := sigma); [eauto|..]. all: intros ? ?; enough (x ∈ dom Gammaᵤ') as D; [domin D; unfold theta; rewrite D|]; [eauto|]. all: eapply Vars_listtyping. 2, 4: eapply in_flat_map; eexists; (intuition eauto). 2: change t with (snd (s, t)); eapply in_map; eauto. 2: change s with (fst (s, t)); eapply in_map; eauto. eapply right_typing, @Hᵤ'. eapply left_typing, @Hᵤ'. + unfold theta; destruct nth eqn: ?; [|eauto]. domin Heqo; eauto. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)