Fix asymmetry of introductions and eliminations

[joshsh]

The term grammar of Hydra's formal data model (Lambda Graph) has a certain asymmetry with respect to introduction and elimination terms. The following type constructors have paired intros and elims:

• Function type (lambda and application terms)
• Record type (records and projections)
• Union type (injections and case statements)
• Wrapper type (wrapped terms and unwrap terms)
• Optional type (nothing and just terms, and foldopt terms)
• List type (list and foldlist terms)
• Map type (map and foldmap terms)
• Annotation type (annotation and unannotation terms)

The following type constructors do not have clear counterparts in the term grammar:

• Variable type
• Forall type
• Type application
• Let type

Furthermore, the following term constructors have no clear counterpart in the type grammar, nor do they pair an elimination form with an introduction form:

• Variable terms
• Let terms
• Constant terms
• Literal terms

Some of these apparent issues can probably be resolved by studying the literature more closely. If there are any real, formal issues to be worked out, then work them out.

[joshsh]

@wisnesky has labeled this state of affairs as a lack of logical harmony.