Require Export Base.
- Inductive Set B := Abbr : B
- | Abst : B
- | Void : B.
+ Inductive Set B := Abbr: B
+ | Abst: B
+ | Void: B.
- Inductive Set F := Appl : F
- | Cast : F.
+ Inductive Set F := Appl: F
+ | Cast: F.
- Inductive Set K := Bind : B -> K
- | Flat : F -> K.
+ Inductive Set K := Bind: B -> K
+ | Flat: F -> K.
- Inductive Set T := TSort : nat -> T
- | TLRef : nat -> T
- | TTail : K -> T -> T -> T.
+ Inductive Set T := TSort: nat -> T
+ | TLRef: nat -> T
+ | TTail: K -> T -> T -> T.
Hint f3KTT : ltlc := Resolve (f_equal3 K T T).
Tactic Definition TGenBase :=
Match Context With
+ | [ H: (TSort ?) = (TSort ?) |- ? ] -> Inversion H; Clear H
+ | [ H: (TLRef ?) = (TLRef ?) |- ? ] -> Inversion H; Clear H
| [ H: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] -> Inversion H; Clear H
| _ -> Idtac.
End s_props.
- Hints Resolve s_le s_lt s_inj.
+ Hints Resolve s_le s_lt s_inj : ltlc.
Tactic Definition SRw :=
Repeat (Rewrite s_S Orelse Rewrite s_plus_sym).