Definition a_or_b (A B:Prop) (p:A \/ B) :=
  match p with
  | or_introl _ => 1
  | or_intror _ => 4
  end.