proposition: Theorem app_nil_r : forall (X : Type) (lst : list X), lst ++ [] = lst.
proof: Proof. intros X lst. induction lst as [ | h t IHt]. - reflexivity. - simpl. rewrite IHt. reflexivity. Qed.
imports: Coq(Arith List) LF(IndProp) Coq(Lia)