proposition: Lemma cl_term_red1 : forall (e : env) (A T : term), typ e A T -> forall B : term, red1 A B -> loose_eqc (cl_term A (class_env e)) (cl_term B (class_env e)).
proof: Proof. simple induction 1; intros; auto with coc core arith datatypes. inversion_clear H1. inversion_clear H1. inversion_clear H2. inversion_clear H6. simpl in |- *. elim loose_eqc_stable with M (TCs class (cl_term T0 (class_env e0)) (class_env e0)) (TCs class (cl_term M' (class_env e0)) (class_env e0)); auto with coc core arith datatypes. elim H1 with M'; auto with coc core arith datatypes. simpl in |- *. replace (TCs class (cl_term T0 (class_env e0)) (class_env e0)) with (class_env (T0 :: e0)); trivial. elim H5 with M'; auto with coc core arith datatypes. elim (cl_term T0 (class_env e0)); auto with coc core arith datatypes. generalize H2 H3; clear H2 H3. inversion_clear H4; intros. elim type_case with e0 (Abs T0 M) (Prod V Ur); intros; auto with coc core arith datatypes. inversion_clear H4. apply inv_typ_prod with e0 V Ur (Srt x); intros; auto with coc core arith datatypes. apply inv_typ_abs with e0 T0 M (Prod V Ur); intros; auto with coc core arith datatypes. simpl in |- *. apply loose_eqc_trans with (cl_term M (class_env (T0 :: e0))). replace (TCs class (cl_term T0 (class_env e0)) (class_env e0)) with (class_env (T0 :: e0)); auto with coc core arith datatypes. elim cl_term_sound with (T0 :: e0) M T1 (Srt s3); intros; auto with coc core arith datatypes. elim (cl_term T0 (class_env e0)); intros. elim s4; elim (cl_term v (class_env e0)); auto with coc core arith datatypes. elim s4; elim (cl_term v (class_env e0)); auto with coc core arith datatypes. elim (cl_term v (class_env e0)); auto with coc core arith datatypes. unfold subst in |- *. apply cl_term_subst with (cl_term T0 (class_env e0)) (class_env e0); auto with coc core arith datatypes. apply cl_term_sound with (Srt s0); auto with coc core arith datatypes. apply type_conv with V s0; auto with coc core arith datatypes. apply inv_conv_prod_l with Ur T1; auto with coc core arith datatypes. simpl in |- *; auto with coc core arith datatypes. discriminate H4. simpl in |- *. elim H4 with N1; intros; auto with coc core arith datatypes. case s1; case s2; elim (cl_term v (class_env e0)); auto with coc core arith datatypes. simpl in |- *. elim (cl_term u (class_env e0)); intros; auto with coc core arith datatypes. case s; elim H1 with N2; auto with coc core arith datatypes. inversion_clear H4. simpl in |- *. elim loose_eqc_stable with U (TCs class (cl_term T0 (class_env e0)) (class_env e0)) (TCs class (cl_term N1 (class_env e0)) (class_env e0)); auto with coc core arith datatypes. elim H1 with N1; auto with coc core arith datatypes. simpl in |- *. replace (TCs class (cl_term T0 (class_env e0)) (class_env e0)) with (class_env (T0 :: e0)); auto with coc core arith datatypes. elim H3 with N2; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType