Section a.
 Variable A:Prop.
 Theorem easy:(B:Prop)B->B.
  Exact ([H:Prop][B:Prop][b:B]b A).
 Qed.
 Section b.
  Theorem easy':(B:Prop)B->B.
   Exact easy.
  Qed.
 End b.
End a.