aboutsummaryrefslogtreecommitdiff
path: root/states/MakeInitial.v
blob: cfc3f5d2ab787de40e31093abb0ce4d9ffb934ca (plain)
1
2
3
4
5
6
7
8
9
Require Export Prelude.
Require Export Logic_Type.
Require Export Logic_TypeSyntax.
Require Export Equality.
Require Export Tauto.
Require Export Inv.
Require Export EAuto.
Require Export Refine.