[coq] fix substitution

Correct:

    (subst i v (pair e1 e2))
    = (pair (subst i (left v) e1) (subst i (right v) e2)

Previously:

    (subst i v (pair e1 e2)) = (pair (subst i v e1) (subst i v e2))
[coq] add exprsize/valsize metrics, and ind/rec schemes
[coq] add eq_xyz_dec theorems for inductive types
[coq] bugfix in the semantics

There was a typo in Lift_App_R, making it:

    (app (pair v1 v2) v) ==> (pair (app v1 (left v)) (app v1 (right v)))

Note the repitition of v1. Fixed.
[coq] lots of changes to operational_semantics.v

Rearrange/rename some things.

Prove some mostly syntactic stuff about branches/pairfree/wff:

    branches are pairfree
    pairfree => leftbranch=rightbranch=identity
    xbranch(ybranch(e)) = ybranch(e)

    pairfree => wff

    subst(pairfree, pairfree) is pairfree
    subst(wff, pairfree) is wff
    subst(pairfree, wff) is wff
    subst(wff, wff) is wff

    step preserves pairfree
    step preserves wff

Prove some lemmas about step:

    values_dont_step, values_not_stuck, steppers_not_stuck

Remove some unnecessary lemmas (left_branch_still_unequal, etc.)

Replace a proof of stuck_or_not using Classical with steps_dec,
is_value_dec, stuck_or_not_dec, with stuck_or_not a simple lift into
Prop.

Prove lemma 3-L. Remove junk at the bottom.