proposition: Lemma T1_injection : forall c c', T1_inj c = T1_inj c' -> c = c'.
proof: Proof. induction c; destruct c';simpl;auto with T2. discriminate 1. discriminate 1. injection 1;auto with T2. rewrite (IHc1 c'1). rewrite (IHc2 c'2). destruct 2;auto with T2. injection H;auto with T2. injection H;auto with T2. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo