File: cycle.v

package info (click to toggle)
prooftree 0.13-2
  • links: PTS, VCS
  • area: main
  • in suites: bookworm, bullseye
  • size: 592 kB
  • sloc: ml: 4,462; sh: 117; makefile: 111
file content (17 lines) | stat: -rw-r--r-- 267 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
 

Lemma a : forall(P1 P2 P3 P4 : Prop), 
  P1 -> P2 -> P3 -> P4 -> P1 /\ P2 /\ P3 /\ P4.
Proof.
  intros P1 P2 P3 P4 H H0 H1 H2.
  repeat split.
        all : swap 1 2.
        all : cycle 2.
        all : revgoals.
        auto.
      auto.
    auto.
  auto.
Qed.