proposition: Lemma liftedEnv_empty : forall E n k, emptyEnv E -> liftedEnv n E k [=] EmptyEnv.
proof: Proof. intros; split; intros p A D. unfold liftedEnv in D. destruct (nth_app (initialSeg E k) (copy n None ++ finalSeg E k) p D) as [[dec cond] | [dec cond]]. set (w := initialSeg_prefix E k p dec). destruct (H p); try_solve. destruct (nth_app (copy n None) (finalSeg E k) (p - length (initialSeg E k)) dec) as [[dec' cond'] | [dec' cond']]. destruct (emptyEnv_copyNone n (p - length (initialSeg E k))); try_solve. set (w := nth_finalSeg_nth E k (p - length (initialSeg E k) - length (copy n (A:=option SimpleType) None))). destruct (H (k + (p - length (initialSeg E k) - length (copy n (None (A:=SimpleType)))))); try_solve. destruct p; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)