proposition: Lemma proj_cont_closed : reflexive succ -> context_closed succ -> context_closed psucc.
proof: Proof. intros Hrefl H. unfold context_closed, proj_ord. induction c; intros. simpl. hyp. simpl. destruct (pi f) as [[k h]|]. rewrite !Vnth_cast, !Vnth_app. case (le_gt_dec i k); intro. case (eq_nat_dec i k); intro. subst. rewrite !Vnth_cons_head; try lia. apply IHc. hyp. gen (Vnth_app_aux (S j) (Vnth_cast_aux e h) l). assert (k-i=S(k-i-1)). lia. rewrite H1. intro. rewrite !Vnth_cons. apply Hrefl. apply Hrefl. rewrite !Vmap_cast, !Vmap_app. simpl. set (d := Cont f e (Vmap proj t) Hole (Vmap proj t0)). change (succ (fill d (proj (fill c t1))) (fill d (proj (fill c t2)))). apply H. apply IHc. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil SN ARelation RelUtil ACompat NatUtil)