The Coq mailing list

[like <12like34xiongmao AT 163.com>]

Hello:
     I want to embed  PPTL(a kind of logic) in Coq. Because of its complex
semantic, I just embed its systax. 
     Inductive formula :Set:=
  | For : formula -> formula -> formula 
  | Fneg: formula -> formula  
  | Fnext: formula -> formula  
  | prj : list formula -> formula->formula.
And then I define some axioms for it.
But I have a problem when proving this, I don't know why.

Axiom t2 :forall(p q:formula),('|-('x p '&&  'x q) )<->('|-('x(p '&& q))).
Theorem tt2 :forall(p q r:formula),('|-('x p '&&  'x q) ; r)->('|-('x(p '&& 
q))
; r).
intros.
rewrite t2 in H.

 Error: Found no subterm matching "'|-'x ?63 '&& 'x ?