-axiom right_mk_tape : ∀sig,ls,c,rs.right ? (mk_tape sig ls c rs) = rs.
-axiom left_mk_tape : ∀sig,ls,c,rs.left ? (mk_tape sig ls c rs) = ls.
-axiom current_mk_tape : ∀sig,ls,c,rs.current ? (mk_tape sig ls c rs) = c.
-axiom length_tail : ∀A,l.0 < |l| → |tail A l| < |l|.
-axiom lists_length_split :
- ∀A.∀l1,l2:list A.(∃la,lb.(|la| = |l1| ∧ l2 = la@lb) ∨ (|la| = |l2| ∧ l1 = la@lb)).
-axiom opt_cons_tail_expand : ∀A,l.l = option_cons A (option_hd ? l) (tail ? l).
-