Section Sekcjunia.

  Variable a b c : nat.

  Let x:=5.
  Let y:=6.
  Let z:=a+c.

  Definition pierwsza := a+c.

  Lemma drugi : z+0=z -> pierwsza=a+c.
  Proof.
    trivial.
  Save.
  
  Print pierwsza.
  Print drugi.

End Sekcjunia.

Print pierwsza.
Print drugi.



Section Druga_Sekcja.

  Variable A:Type.

  Let w := nat.

  Inductive List : Type := nil : w -> List | cons : A -> List -> List.

  Definition singl x := cons x (nil 0).

  Definition head l a := 
    match l with 
    | nil _ => singl a 
    | cons x _ => singl x 
    end.

  Print List.
  Check nil.
  Check cons.
  Print singl.
  Print head.

  Hint Resolve nil.

  Print Hint List.

End Druga_Sekcja.

Print List.
Check nil.
Check cons.
Print singl.
Print head.

Print Hint List.