The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,


 Let us look at your goal with "Printing Notations" off


Unset Printing Notations.

(*
1 subgoal (ID 30)

  p : formula
  q : formula
  r : formula
  H : model_p (chop (and (Fnext p) (Fnext q)) r)
  ============================
   model_p (chop (Fnext (and p q)) r)
*)

Check t2.
(*t2
     : forall p q : formula,
       Logic.iff (model_p (and (Fnext p) (Fnext q)))
         (model_p (Fnext (and p q)))

*)

If you consider some instance  (t2 X Y) of t2
its type is Logic.iff (model_p (and (Fnext X) (Fnext Y)))
         (model_p (Fnext (and X Y)))

but the left hand side of this equivalence is not a subterm of H
(the structure induced by model_p , chop, Fnext ... is not compatible).

Pierre