A data structure for sets of trees. Tries allow for efficient storage of lists of elements.  The prefixes are shared so it is space efficient.

I am looking for a similar way to efficiently store trees.  I would like to be able to check for membership and to add elements, knowing if a given tree is a subtree of some stored trees or if there exists a stored tree being a subtree of the given tree is also desirable.

I would typically store about 500 unbalanced binary trees of height less than 50.

EDIT

My application is some kind of model checker using some sort of memoization. Imagine I have a state $s$ and the following formulae: $f = \phi$ and $g = (\phi \vee \psi)$ with $\phi$ being a complex subformula, and imagine I first want to know if $f$ holds in $s$.  I check if $\phi$ holds and after a lengthy process I obtain that it is the case. Now, I want to know if $g$ holds in $s$. I would like to remember the fact that $f$ holds and to notice that $g \Rightarrow f$ so that I can derive $g$ in $s$ almost instantly.
Conversely, if I have proved that $g$ does not hold in $t$, then I want to tell that $f$ does not hold in $t$ almost instantly.

We can build a partial order on formulae, and have $g \geq f$ iff $g \Rightarrow f$.  For each state $s$, we store two sets of formulae; $L(s)$ stores the maximal formulae that hold and $l(s)$ stores the minimal formulae that do not hold. Now given a state $s$ and a formula $g$, I can see if $\exists f \in L(s), f \Rightarrow g$, or if $\exists f \in l(s), g \Rightarrow f$ in which case I am done and I know directly whether $g$ holds in $s$.

Currently, $L$ and $l$ are implemented as lists and this is clearly not optimal because I need to iterate through all stored formulae individually. If my formulae were sequences, and if the partial order was "is a prefix of" then a trie could prove much faster. Unfortunately my formulae have a tree like structure based on $\neg, \wedge$, a modal operator, and atomic propositions.

As @Raphael and @Jack points out, I could sequentialise the trees, but I fear it would not solve the problem because the partial order I am interested in would not correspond to "is a prefix of".
You might want to check out g-tries. This is essentially the data structure you're looking for, but designed for use with general graphs instead of just trees. As such, I'm not sure that g-tries have good theoretical guarantees -- I think they use a graph canonization algorithm as a subroutine -- but in practice they seem to work well.

(Don't be scared that the linked paper is about "network motifs in biological networks": the g-trie is a perfectly good abstract data structure for graphs.)