proposition: Lemma canonical_forms: forall v t, nil ⊢ v ∈ t -> isvalue v -> match t with | Bool => exists b, v = Const b | Fun t1 t2 => exists x a, v = Abs x a end.
proof: Proof. intros v t TY VAL. inversion VAL; subst; inversion TY; subst. - exists x, a; auto. - exists b; auto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)