Notación:    E(G) |-  t:T significa que el término t está bien tipado y tiene tipo T en el
entorno E y contexto G.
WF(E) [G] significa que el entorno E está bien formado y que el contexto G es válido
en este entorno.
 

                           WF(E) [G]    (x:T) Î G                                   WF(E)[G]    (c:T) Î E
Regla Var           --------------------------           Regla Const      -------------------------- 
                                  E(G) |-  x:T                                                         E(G) |-  c:T
 
Ejemplo: táctica Assumption:
Mira en el contexto local si hay una hipótesis con tipo igual que el objetivo:

Coq < Variable A:Prop.
A is assumed
Coq < Lemma var: A->A.
1 subgoal

  ============================
   A->A
var < Intro.
1 subgoal
  H : A
  ============================
   A
var < Assumption.
Subtree proved!
 

                            E[G]|- (x:T)U : s   E[G ::(x:T)]|- t:U
Regla Lam          ----------------------------------------
                                  E(G) |-  [x:T]t : (x:T)U

                            E[G]|- "x:T·U : s   E[G ::(x:T)]|- t:U
es decir:              ----------------------------------------
                                  E(G) |-  lx:T·t :  "x:T·U

En el caso no dependiente se escribe  E(G) |-  lx:T·t : T®U.
 
Ejemplo: táctica Intro:

Variable P,Q:nat->Prop.
P is assumed
Q is assumed
Variable R:nat->nat->Prop.
R is assumed
Lemma PQR:(x,y:nat)((R x x)->(P x)->(Q x))->(P x)->(R x y)
->(Q x).
1 subgoal

  ============================
   (x,y:nat)((R x x)->(P x)->(Q x))->(P x)->(R x y)->(Q x)
Intros.
1 subgoal

  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (Q x)

                            E[G]|- t:(x:U)T     E[G]|- u:U
Regla App           --------------------------------
                                  E(G) |-  (t u) : T{x/u}

 
                           E[G]|- t: ("x:U·T)     E[G]|- u:U
o sea                   ------------------------------------
                                  E(G) |-  (t u) : T{x/u}

                                             E[G]|- t: (U®T)     E[G]|- u:U
En el caso independiente :  ------------------------------------
                                                      E(G) |-  (t u) : T

Ejemplo: táctica Cut (implementa el caso independiente):
Si tenemos la situación siguiente:
  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (P x)->(Q x)

PQR < Cut (R x x).
2 subgoals

  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (R x x)->(P x)->(Q x)

subgoal 2 is:
 (R x x)

Ejemplo: táctica Change : si partimos de:
 
  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (Q x)

PQR < Change (([n:nat](Q n)) x).
1 subgoal

  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   ([n:nat](Q n) x)