include "ASM/JMCoercions.ma". (* This contains rather more than we really want. *)

notation "hvbox(« term 19 a, break term 19 b»)" 
with precedence 90 for @{ (dp ?? $a $b) }.

lemma use_sig : ∀A:Type[0]. ∀P:A → Prop. ∀x:Σx:A.P x. P x.
#A #P * #a #p @p
qed.