conversion.v 592 Bytes
Newer Older
Gaspard Ferey's avatar
Gaspard Ferey committed
1 2

Require Import LPTerm.
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
3
Require Import WF.
Gaspard Ferey's avatar
Gaspard Ferey committed
4 5 6 7 8 9 10


Lemma inversion_rel : forall Γ t u, Γ  -> t  u  Γ -> exists s A Δ, Δ  t : A /\ Δ  u : A /\ Δ  A : s.
Proof.
  intros.
  induction Γ.
  - inversion H0.
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
11 12
  - inversion H.
    subst. inversion H0 ; subst. apply IHΓ.
Gaspard Ferey's avatar
Gaspard Ferey committed
13
    + eapply vardecl_WF. apply H.
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
14
    + easy.
Gaspard Ferey's avatar
Gaspard Ferey committed
15
    + eapply IHΓ. eapply  vardecl_WF . apply H. inversion H0. subst. easy.
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
16 17
  - inversion H0; subst.
    inversion H ; subst.
Gaspard Ferey's avatar
Gaspard Ferey committed
18 19 20
    + exists s,A,Γ.
      split. apply H5.
      split. apply H6. apply H4.
Gaspard Ferey's avatar
Gaspard Ferey committed
21
    + apply IHΓ. eapply ruldecl_WF. apply H. easy.
Gaspard Ferey's avatar
Gaspard Ferey committed
22
Qed.
Gaspard Ferey's avatar
Gaspard Ferey committed
23 24