summaryrefslogtreecommitdiff
path: root/test-suite/output/CompactContexts.out
blob: 9d1d19877ee777b259f80962be44b33ebf2a2080 (plain)
1
2
3
4
5
6
7
1 subgoal
  
  hP1 : True
  a : nat   b : list nat   h : forall x : nat, {y : nat | y > x}
  h2 : True
  ============================
  False