Full proof for my answer to https://stackoverflow.com/questions/44059569/

nodup_app_disjoint.v

(* https://stackoverflow.com/questions/44059569/coq-goal-variable-not-transformed-by-induction-when-appearing-on-left-side-of-a/ *)

Require Import Coq.Lists.List.
Import ListNotations.

Inductive Disjoint {X : Type}: list X -> list X -> Prop :=
  | disjoint_nil: Disjoint [] []
  | disjoint_left: forall x l1 l2, Disjoint l1 l2 -> ~(In x l2) -> Disjoint (x :: l1) l2
  | disjoint_right: forall x l1 l2, Disjoint l1 l2 -> ~(In x l1) -> Disjoint l1 (x :: l2).
Hint Constructors Disjoint.

Lemma disjoint_cons_l {X} (h : X) l1 l2 :
  Disjoint (h :: l1) l2 -> Disjoint l1 l2.
Proof.
  intros H; remember (h :: l1) as hl1 eqn:E.
  induction H; inversion E; subst; intuition.
Qed.

Lemma disjoint_singleton {X} h (l : list X) :
  Disjoint [h] l -> ~ In h l.
Proof.
  intro F; remember [h] as s eqn: E.
  induction F; inversion E; subst; firstorder.
Qed.

Theorem nodup_app__disjoint {X} (l: list X) :
  (forall l1 l2, l = l1 ++ l2 -> Disjoint l1 l2) -> NoDup l.
Proof.
  induction l as [| h l]; intros F.
  - constructor.
  - constructor.
    + specialize (F [h] l eq_refl).
      now apply disjoint_singleton.
    + apply IHl; clear IHl; intros l1 l2 Happ.
      subst; specialize (F (h :: l1) l2 eq_refl).
      now apply disjoint_cons_l in F.
Qed.