diff options
Diffstat (limited to 'theories/Program/Subset.v')
| -rw-r--r-- | theories/Program/Subset.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 1c89b6c3b1..ae366204ac 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -73,10 +73,10 @@ Proof. simpl. split ; intros ; subst. - inversion H. - reflexivity. + - inversion H. + reflexivity. - pi. + - pi. Qed. (* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f] |