blob: 1e0a6187620990c5cbddf274463d97b13cde3ab5 (
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
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* Xavier Leroy INRIA Paris-Rocquencourt *)
(* David Monniaux CNRS, VERIMAG *)
(* Cyril Six Kalray *)
(* *)
(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
Set Implicit Arguments.
Theorem and_dec : forall A B C D : Prop,
{ A } + { B } -> { C } + { D } ->
{ A /\ C } + { (B /\ C) \/ (B /\ D) \/ (A /\ D) }.
Proof.
intros A B C D AB CD.
destruct AB; destruct CD.
- left. tauto.
- right. tauto.
- right. tauto.
- right. tauto.
Qed.
|
