Library Lambda.TPOSR.Unlab


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Env.

Require
 Import
 Lambda.TPOSR.Terms.

Require
 Import
 Lambda.TPOSR.Reduction.

Require
 Import
 Lambda.TPOSR.Conv.

Require
 Import
 Lambda.TPOSR.LiftSubst.

Require
 Import
 Lambda.TPOSR.Env.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

Implicit
 Types
 A
 B
 M
 N
 T
 t
 u
 v
 : lterm.

Implicit
 Types
 e
 f
 g
 : lenv.







Fixpoint
 unlab (t
 : lterm) : term :=

  match
 t
 with


  | Srt_l s
 ⇒ Srt s


  | Ref_l n
 ⇒ Ref n


  | Abs_l T
 t
 ⇒ Abs (unlab T
) (unlab t
)

  | App_l T
 u
 v
 ⇒ App (unlab u
) (unlab v
)

  | Pair_l T
 u
 v
 ⇒ Pair (unlab T
) (unlab u
) (unlab v
)

  | Prod_l T
 U
 ⇒ Prod (unlab T
) (unlab U
)

  | Sum_l T
 U
 ⇒ Sum (unlab T
) (unlab U
)

  | Subset_l T
 U
 ⇒ Subset (unlab T
) (unlab U
)

  | Pi1_l T
 t
 ⇒ Pi1 (unlab t
)

  | Pi2_l T
 t
 ⇒ Pi2 (unlab t
)

  end
.




Fixpoint
 unlab_ctx (t
 : lenv) : env :=

  match
 t
 with


  | nil ⇒ nil

  | cons A
 tl
 ⇒ cons (unlab A
) (unlab_ctx tl
)

 end
.




Notation
 "| t |" := (unlab t
) (at
 level
 70).




Lemma
 lab_lift_rec : ∀ M
 n
 k
, |llift_rec n
 M
 k
| = lift_rec n
 (|M|) k
.




Lemma
 lab_lift : ∀ M
 n
, |llift n
 M
| = lift n
 (|M|).




Lemma
 lab_subst_rec : ∀ M
 N
 k
, |lsubst_rec M
 N
 k
| = subst_rec (|M|) (|N|) k
.




Lemma
 lab_subst : ∀ M
 N
, |lsubst M
 N
| = subst (|M|) (|N|).




Lemma
 unlab_lred : ∀ M
 N
, lred1 M
 N
 → red (|M|) (|N|).




Lemma
 unlab_lab_red1 : ∀ (M
 : lterm) (N
 : term), red1 (|M|) N
 → 

  ∃ N'
, |N'| = N
 ∧ lred1 M
 N'
.




Lemma
 unlab_lab_red : ∀ (M
 : lterm) (N
 : term), red (|M|) N
 → 

  ∃ N'
, |N'| = N
 ∧ lred M
 N'
.




Lemma
 unlab_lab_par_red1 : ∀ (M
 : lterm) (N
 : term), par_red1 (|M|) N
 → 

  ∃ N'
, |N'| = N
 ∧ par_lred1 M
 N'
.




Lemma
 conv_unlab_conv : ∀ U
 V
, conv U
 V
 → Lambda.Reduction.conv (unlab U
) (unlab V
).