proposition: Lemma S1_decrease: forall u l l', S1 u l l' -> exists a, ltM a (h2ol l') (h2ol l).
proof: Proof. induction 1. simpl. exists zero. apply ltM_tail;auto. simpl. exists zero. unfold ltM. split. Opaque T1_eq_dec. simpl; case (T1_eq_dec (h2o h) zero). intro e; rewrite e; simpl. case (T1_eq_dec zero zero). auto with arith. intros; absurd (zero=zero);auto. case (T1_eq_dec zero (h2o h)). intros; absurd (zero = h2o h);auto. case (T1_eq_dec zero zero). auto. intro; absurd (zero=zero). auto. auto. simpl. intros;case (T1_eq_dec b (h2o h)). intros;case (T1_eq_dec b zero). intro; clear e; subst b; inversion H. auto. intros;case (T1_eq_dec b zero). intro; subst b; inversion H. auto. simpl. case IHS1; intros a Ha;exists a; apply ltM_cons;auto. Qed.
imports: Arith Omega List EPSILON0 MSE0