Inductive nat: Type :=
| O: nat
| S: nat -> nat.

Recursive plusnat (x: nat) y [0] : _ :=
   match x with
     | y
     | \(x: nat). S (plusnat x y).

Overload plus with plusnat [0].

Inductive list A : _ :=
| nil: list A
| conc: A -> list A -> list A.

Implicite nil [1].
Implicite conc [1].

Recursive app A (l1: list A) l2 [1] : _ :=
   match l1 with
     | \A. l2
     | \A. \e. \l1. conc e (app _ l1 l2).

Implicite app [1].

Overload plus with @app [1].

Inductive eq A a : A -> Type :=
| eqrefl: eq A a a.

Implicite eq [1].
Implicite eqrefl [1].

Definition anytolist := (\A. \(x:A). conc x nil).

Coercion anytolist [1].

Show Definitions.
Show Coercions.

Typecheck (plus O nil).

Simpl (plus O nil).

Simpl (anytolist nat O).