Comment by JonChesterfield

I can't tell if this is pseudocode or what proof in coq usually looks like:

Theorem NestedTreeContains1:

  forall (t: tree),
    t = Node example 2 (Node Nil 3 Nil) 

  -> 

    contains 1 t = true.

Proof.

nail.

wreck t.

- wat.

- wreck H into Ht1, Hv and Ht2.

  sub Hv.
  evaluate.
  sub Ht1.
  just ExampleTreeContains1.

Qed.

Theorem, forall, qed look fairly likely. Are there built-in operations in coq called 'wat' and 'wreck'?