Library Lambda.InvLiftSubst


Require
 Import
 Lambda.Utils.

Require
 Import
 Lambda.Tactics.




Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.Conv_Dec.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Env.







Lemma
 inv_lift_prod : ∀ t
 U
 V
 n
, lift n
 t
 = Prod U
 V
 →

 ∃ U'
, ∃ V'
, t
 = Prod U'
 V'
 ∧ U
 = (lift_rec n
 U'
 0) ∧ V
 = (lift_rec n
 V'
 1).




Lemma
 inv_lift_sum : ∀ t
 U
 V
 n
, lift n
 t
 = Sum U
 V
 →

 ∃ U'
, ∃ V'
, t
 = Sum U'
 V'
 ∧ U
 = (lift_rec n
 U'
 0) ∧ V
 = (lift_rec n
 V'
 1).




Lemma
 inv_lift_subset : ∀ t
 U
 V
 n
, lift n
 t
 = Subset U
 V
 →

 ∃ U'
, ∃ V'
, t
 = Subset U'
 V'
 ∧ U
 = (lift_rec n
 U'
 0) ∧ V
 = (lift_rec n
 V'
 1).




Lemma
 inv_lift_abs : ∀ t
 U
 V
 n
, lift n
 t
 = Abs U
 V
 →

 ∃ U'
, ∃ V'
, t
 = Abs U'
 V'
 ∧ U
 = (lift_rec n
 U'
 0) ∧ V
 = (lift_rec n
 V'
 1).




Lemma
 inv_lift_app : ∀ t
 U
 V
 n
, lift n
 t
 = App U
 V
 →

 ∃ U'
, ∃ V'
, t
 = App U'
 V'
 ∧ U
 = (lift_rec n
 U'
 0) ∧ V
 = (lift_rec n
 V'
 0).




Lemma
 inv_lift_pair : ∀ t
 U
 V
 W
 n
, lift n
 t
 = Pair U
 V
 W
 →

 exists3
 U'
 V'
 W'
, t
 = Pair U'
 V'
 W'
 ∧ U
 = (lift_rec n
 U'
 0) ∧ V
 = (lift_rec n
 V'
 0) ∧ W
 = (lift_rec n
 W'
 0).




Lemma
 inv_lift_pi1 : ∀ t
 U
 n
, lift n
 t
 = Pi1 U
 →

 ∃ U'
, t
 = Pi1 U'
 ∧ U
 = (lift_rec n
 U'
 0).




Lemma
 inv_lift_pi2 : ∀ t
 U
 n
, lift n
 t
 = Pi2 U
 →

 ∃ U'
, t
 = Pi2 U'
 ∧ U
 = (lift_rec n
 U'
 0).




Lemma
 inv_lift_sort : ∀ t
 s
 n
, lift n
 t
 = Srt s
 → t
 = Srt s
.




Lemma
 inv_subst_sort : ∀ t
 t'
 n
 s
, subst_rec t
 t'
 n
 = Srt s
 → 

  t
 = Srt s
 ∨ t'
 = Srt s
.