astrolabe.v

Section astrolabe. 
  Variable A : Type.
  Variable open close : A.
  Variable l1 l2 : list A.
  Variable wp : list A -> Prop.

  Goal wp (open :: ((l1 ++ close :: nil) ++ l2)%list) -> 
  wp (open :: (l1 ++ close :: l2)%list) .
    match goal with
    | [ |- ?p ?a -> ?p ?b ] => 
      let H := fresh "H" in 
      cut (a = b); [solve[intro H; rewrite H; auto]|]
    end.
    (* goal is now:
         (open :: (l1 ++ close :: nil) ++ l2)%list =
         (open :: l1 ++ close :: l2)%list
    *)
  Admitted.
End astrolabe.