proposition: Lemma incl_nth_error {X: Type} {Gamma Gamma': list X} : incl Gamma Gamma' -> exists ξ, forall x, nth_error Gamma x = nth_error Gamma' (ξ x).
proof: Proof. elim: Gamma Gamma'. - move=> Gamma' _. exists (fun x => length Gamma'). move=> [|x] /=; apply /esym; by apply /nth_error_None. - move=> x Gamma IH Gamma'. move=> /Forall_forall /Forall_cons_iff. move=> [/(@In_nth_error _ _ _) [nx] Hnx /Forall_forall /IH] [ξ Hξ]. exists (fun y => if y is S y then ξ y else nx). by case. Qed.
imports: List Lia ssreflect ssrbool ssrfun