Library Coq.Wellfounded.Disjoint_Union

Author: Cristina Cornes From : Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355

Require Import Relation_Operators.

Section Wf_Disjoint_Union.
  Variables A B : Type.
  Variable leA : A -> A -> Prop.
  Variable leB : B -> B -> Prop.

  Notation Le_AsB := (le_AsB A B leA leB).

  Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x).

  Lemma acc_B_sum :
    well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x).

  Lemma wf_disjoint_sum :
    well_founded leA -> well_founded leB -> well_founded Le_AsB.

End Wf_Disjoint_Union.