proposition: Lemma red_item : forall n t e, item_lift t e n -> forall f, red1_in_env e f -> item_lift t f n \/ (forall g, trunc _ (S n) e g -> trunc _ (S n) f g) /\ ex2 (fun u => red1 t u) (fun u => item_lift u f n).
proof: Proof. simple induction n. do 3 intro. elim H. do 4 intro. rewrite H0. inversion_clear H1. intros. inversion_clear H1. right. split; intros. inversion_clear H1; auto with coc core arith datatypes. exists (lift 1 u). unfold lift in |- *; auto with coc core arith datatypes. exists u; auto with coc core arith datatypes. left. exists x; auto with coc core arith datatypes. do 5 intro. elim H0. do 4 intro. rewrite H1. inversion_clear H2. intros. inversion_clear H2. left. exists x; auto with coc core arith datatypes. elim H with (lift (S n0) x) l f0; auto with coc core arith datatypes; intros. left. elim H2; intros. exists x0; auto with coc core arith datatypes. rewrite simpl_lift. pattern (lift (S (S n0)) x0) in |- *. rewrite simpl_lift. elim H5; auto with coc core arith datatypes. right. elim H2. simple induction 2; intros. split; intros. inversion_clear H9; auto with coc core arith datatypes. elim H8; intros. exists (lift (S (S n0)) x1). rewrite simpl_lift. pattern (lift (S (S n0)) x1) in |- *. rewrite simpl_lift. elim H9; unfold lift at 1 3 in |- *; auto with coc core arith datatypes. exists x1; auto with coc core arith datatypes. exists x; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList