# Module `Cc_plugin.Ccproof`

`type rule`

`=`

`|`

`Ax of Ccalgo.axiom`

if ⊢ t = u :: A, then ⊢ t = u :: A

`|`

`SymAx of Ccalgo.axiom`

if ⊢ t = u : A, then ⊢ u = t :: A

`|`

`Refl of Ccalgo.ATerm.t`

`|`

`Trans of proof * proof`

⊢ t = u :: A -> ⊢ u = v :: A -> ⊢ t = v :: A

`|`

`Congr of proof * proof`

⊢ f = g :: forall x : A, B -> ⊢ t = u :: A -> f t = g u :: B

`t`

Assumes that B`t`

≡ B`u`

for this to make sense!`|`

`Inject of proof * Constr.pconstructor * int * int`

⊢ ci v = ci w :: Ind(args) -> ⊢ v = w :: T where T is the type of the n-th argument of ci, assuming they coincide

`and proof`

`= private`

`{`

`p_lhs : Ccalgo.ATerm.t;`

`p_rhs : Ccalgo.ATerm.t;`

`p_rule : rule;`

`}`

`val build_proof : Environ.env -> Evd.evar_map -> Ccalgo.forest -> [ `Discr of int * Ccalgo.pa_constructor * int * Ccalgo.pa_constructor | `Prove of int * int ] -> proof`