proposition: Lemma Sh_head : forall n o h h', Sh n o h h' -> head_at_l h o = true.
proof: Proof. destruct 1. eapply S1_head; eauto. eapply S2_head. eauto. elim s. simpl. intros;eapply Rn_head;eauto. simpl. intros;eapply Rn_head;eauto. simpl; auto. Qed.
imports: Arith Omega List EPSILON0 MSE0