blob: 6a5153339d7dc37a94fa06dd45f11d3f2a29a9e4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: Inclusion.v,v 1.1.2.1 2004/07/16 19:31:41 herbelin Exp $ i*)
(** Author: Bruno Barras *)
Require Relation_Definitions.
Section WfInclusion.
Variable A:Set.
Variable R1,R2:A->A->Prop.
Lemma Acc_incl: (inclusion A R1 R2)->(z:A)(Acc A R2 z)->(Acc A R1 z).
Proof.
NewInduction 2.
Apply Acc_intro;Auto with sets.
Qed.
Hints Resolve Acc_incl.
Theorem wf_incl:
(inclusion A R1 R2)->(well_founded A R2)->(well_founded A R1).
Proof.
Unfold well_founded ;Auto with sets.
Qed.
End WfInclusion.
|
