proposition: Lemma lex_lifting_aux : forall n (l : list ES.A), length l = n -> Accs r l -> Restricted_acc (Accs r) lex l.
proof: Proof. intro n; induction n as [ | n IHn]; intros l Hl HAccs. destruct l; [constructor | inversion Hl]. intros l' Hl' Hlex; inversion Hlex. destruct l as [ | h l]; [inversion Hl | idtac]. assert (acc_h : Acc r h). apply HAccs; left; trivial. assert (Accs_l : forall (a : ES.A), In a l -> Acc r a). intros s s_in_l; apply HAccs; right; trivial. assert (Hl2 : length l = n). inversion Hl; trivial. gen (IHn l Hl2 Accs_l). clear Hl HAccs. generalize dependent l. induction acc_h as [h acc_h IHh]. intros l Accs_l Hl Hacc. induction Hacc as [l Hacc IHl]. constructor. intros l' Hl' Hlex. destruct l' as [ | h' l']. inversion Hlex. assert (Accs_l' : forall (a : ES.A), In a l' -> Acc r a). intros t Ht; apply Hl'; right; trivial. clear Hl'. inversion Hlex; subst. apply IHh; trivial. apply IHn; trivial. apply IHl; trivial. cut (length (h :: l') = length ( h :: l)). simpl; auto with arith. gen Hlex; apply lex_length. Qed.
imports: CoLoR(RelExtras ListUtil AccUtil LogicUtil)