Fixing the lack of the else formulas in the coq model.
Adding support for multiple patterns in the same type rule for the coq model transformation.
From “well typed” to “has type”, to follow the rest of the model

It’s still “well_typed” in Pierre’s proofs, but I think we agreed a long time ago to rename those.
Fixing the pattern for final types with constructors.

I.e. Functions, which have type FunType(t1,t2)