Further fix for #3213

[mtzguido]

Followup of #3213 and #3214. Given forall x1 .. xn. p x1 .. xn we cannot rewrite p to fun x1 .. xn -> True even if the types match, or we can also obtain an inconsistentency:

let also_bad ()
  : Lemma (forall (f : (nat -> Type0)). (forall (x : nat). f x) ==> (fun (_:nat) -> True) == f) = ()
  
let eq_fun (f1 f2 : 'a -> 'b) (x : 'a) (_ : squash (f1 == f2)) : Lemma (f1 x == f2 x) = ()

let bad2 () =
  let f0 : int -> Type0 = fun x -> True in
  let f1 : int -> Type0 = fun x -> x >= 0 in
  also_bad ();
  let f0' : nat -> Type0 = f0 in
  let f1' : nat -> Type0 = f1 in
  forall_elim #(nat -> Type0) (fun f -> (forall (x : nat). f x) ==> (fun (_:nat) -> True) == f) f0';
  forall_elim #(nat -> Type0) (fun f -> (forall (x : nat). f x) ==> (fun (_:nat) -> True) == f) f1';
  assert (f0' == (fun (_:nat) -> True));
  assert (f1' == (fun (_:nat) -> True));
  assert (eq2 #(nat -> Type0) f0' f0);
  assert (eq2 #(nat -> Type0) f1' f1);
  assert (f0 == f1);
  eq_fun f0 f1 (-1) ();
  assert False;
  ()

This PR makes it so that we only rewrite full applications of p to n arguments into True.