Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

x: + Formula. h(x)

Applied Tactic: D 0 THENA Auto THEN D (-1)
Generated subgoals:

1. h(inl x1 )

2. h(inr y )