proposition: Lemma nth_pred Γ' Γ U n : n > length Γ' -> nth (pred n) (Γ' @ Γ) unit = nth n (Γ' @ (U :: Γ)) unit.
proof: Proof. revert_until Γ'. induction Γ'; intros. destruct n; auto. depelim H. destruct n; auto. simpl pred. simpl. rewrite <- IHΓ'. destruct n; auto. simpl in H. depelim H. depelim H. simpl in *; lia. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid Arith Wf_nat