blob: 260a539c7311bac9196eb82666f1d7570743f017 (
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
|
(* $Id$ *)
(****************************************************************************)
(* 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.
Induction 2;Intros.
Apply Acc_intro;Auto with sets.
Save.
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.
Save.
End WfInclusion.
|
