fact: Fixpoint door_to_door (cells : seq cell) (i1 i2 : nat) (opt_source opt_target : option pt)(tl : seq nat) : seq (annotated_point * annotated_point) := match tl with | nil => nil | i3 :: nil => to_next_door opt_source opt_target cells i1 i2 i3 | i3 :: tl' => let tail_path := door_to_door cells i2 i3 None opt_target tl' in to_next_door opt_source None cells i1 i2 i3 ++ tail_path end.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL