proposition: Lemma Rn_head : forall n o h h', Rn n o h h' -> head_at h o = true.
proof: Proof. intros n o h h0 H. pattern o, h, h0, H. elim H using Rn_rect2 with (P0 := fun o h h0 (H: Sn n o h h0) => head_at_l h o = true); simpl;auto. intros. generalize (S2_head n u l l' s). simpl. auto. Qed.
imports: Arith Omega List EPSILON0 MSE0