# Module `Rtauto_plugin.Proof_search`

`type form`

`=`

`|`

`Atom of int`

`|`

`Arrow of form * form`

`|`

`Bot`

`|`

`Conjunct of form * form`

`|`

`Disjunct of form * form`

`type proof`

`=`

`|`

`Ax of int`

`|`

`I_Arrow of proof`

`|`

`E_Arrow of int * int * proof`

`|`

`D_Arrow of int * proof * proof`

`|`

`E_False of int`

`|`

`I_And of proof * proof`

`|`

`E_And of int * proof`

`|`

`D_And of int * proof`

`|`

`I_Or_l of proof`

`|`

`I_Or_r of proof`

`|`

`E_Or of int * proof * proof`

`|`

`D_Or of int * proof`

`|`

`Pop of int * proof`

`type state`