typechecker: fix inconsistent simplifications
typechecker: fix inconsistent simplifications

We were simplifying

	forall (x:A). False  --->  False
	exists (x:A). True   --->  True

both of these are only valid if A is inhabited. Both of these lead to a
contradiction:

1)	let a () : Lemma (~ (forall (x:False). False)) = ()

	let b () : Lemma (forall (x:False). False) =
	    FStar.Classical.forall_intro #False #(fun (f:False) -> False) (fun (f:False) -> ())

	let oops () : Lemma False =
	    a (); b ()

2)	let a () : Lemma (exists (x:False). True) =
	    ()

	val ff : #a:Type -> #p:(a -> Type) -> (unit -> Lemma (exists (x:a). p x)) -> Lemma a
	let ff #a #p l = l ()

	let oops () : Lemma False =
	    ff #False #(fun f -> True) a

FStarLang/FStar,FStarLang/FStar,A-Manning/FStar,FStarLang/FStar,A-Manning/FStar,A-Manning/FStar