proposition: Lemma find_sub_of_asub : forall s n v, find v (sub_of_asub s n) = if bgt_nat n v then Some (term_of_aterm (s v)) else None.
proof: Proof. induction n; intros. refl. simpl sub_of_asub. simpl more_list.find. rewrite IHn. unfold eq_var_bool. case_beq_nat v n. assert (bgt_nat (S v) v = true). rewrite bgt_nat_ok. lia. rewrite H. refl. case_eq (bgt_nat n v); intros; case_eq (bgt_nat (S n) v); intros. refl. rewrite bgt_nat_ok in H0. rewrite bgt_nat_ko in H1. lia. rewrite bgt_nat_ok in H1. rewrite bgt_nat_ko in H0. rewrite (beq_ko beq_nat_ok) in H. lia. refl. Qed.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil) CoLoR(NatUtil) Coq(List Relations) CoLoR(term SN ASubstitution)