proposition: Lemma route_cons : forall r r' d, r =r= r' -> d::r =r= d::r'.
proof: Proof. intros r r' d H P;destruct d;simpl;rewrite H;reflexivity. Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia