proposition: Lemma envSubst_dec : forall i Q, {j: nat | envSub Q i j} + {forall j, ~envSub Q i j}.
proof: Proof. assert (H: forall s i Q, {j: nat | envSub Q i j} + {forall j, j < s -> ~envSub Q i j}). induction s. right; intros; lia. intros. destruct (IHs i Q) as [[j Qij] | Qn]. left; exists j; trivial. destruct (envSub_dec Q i s). left; exists s; trivial. right; intros j js. destruct (le_gt_dec s j). assert (j_s: j = s); [lia | rewrite j_s; trivial]. apply Qn; trivial. intros i Q. destruct (H (size Q) i Q) as [[j Qij] | Qn]. left; exists j; trivial. right; intros j. destruct (le_gt_dec (size Q) j). intro Qij. absurd (j < size Q). lia. destruct (sizeOk Q i j); trivial. apply Qn; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)