diff options
Diffstat (limited to 'theories/Wellfounded/Disjoint_Union.v')
| -rw-r--r-- | theories/Wellfounded/Disjoint_Union.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index ac3233704..6e9cbf062 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -19,7 +19,7 @@ Variable A,B:Set. Variable leA: A->A->Prop. Variable leB: B->B->Prop. -Syntactic Definition Le_AsB := (le_AsB A B leA leB). +Notation Le_AsB := (le_AsB A B leA leB). Lemma acc_A_sum: (x:A)(Acc A leA x)->(Acc A+B Le_AsB (inl A B x)). Proof. |